diff --git a/research/p104-present-head-flag1-audit/CERTIFICATE.json b/research/p104-present-head-flag1-audit/CERTIFICATE.json new file mode 100644 index 0000000000..e9575631b1 --- /dev/null +++ b/research/p104-present-head-flag1-audit/CERTIFICATE.json @@ -0,0 +1,185 @@ +{ + "schema_version": 1, + "claim_id": "p104-present-head-flag1-audit", + "pinned_main": "6f100d4bb5083f8c35d96fd95a539811c62f245c", + "flag_index": 1, + "source": 0, + "target": 7, + "basis_head": 232, + "departure_choice": 1, + "arrival_choice": 1, + "basis": [ + 232, + 256, + 7, + 11, + 19, + 35, + 64, + 2, + 1 + ], + "source_register": "X0", + "target_register": "Y7", + "source_initial": [ + 232 + ], + "source_final": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + "target_initial": [], + "target_final": [ + 484, + 232, + 12, + 55, + 75, + 24, + 7, + 2 + ], + "source_initial_is_basis_head": true, + "target_final_contains_basis_head": true, + "source_frame_restored": false, + "target_frame_restored": false, + "source_rank_initial": 1, + "source_rank_final": 9, + "target_rank_initial": 0, + "target_rank_final": 8, + "source_first_event": 591, + "source_last_event": 3954, + "target_first_event": 19, + "target_last_event": 3473, + "source_event_count": 17, + "target_event_count": 9, + "joint_source_target_events": 0, + "basis_head_drop_event": 591, + "basis_head_drop_before": [ + 232 + ], + "basis_head_drop_after": [ + 8, + 32, + 64, + 128, + 256 + ], + "basis_head_arrive_event": 3473, + "basis_head_arrive_before": [ + 95, + 486 + ], + "basis_head_arrive_after": [ + 2, + 7, + 12, + 24, + 55, + 75, + 232, + 484 + ], + "hosting_gap_events": 2882, + "source_annotations_containing_basis_head": 1, + "target_annotations_containing_basis_head": 1, + "target_preterminal_annotations_containing_basis_head": 0, + "source_head_annotations": [ + { + "event": 591, + "opcode": "transport", + "role": "before", + "frame": [ + 232 + ] + } + ], + "target_head_annotations": [ + { + "event": 3473, + "opcode": "transport", + "role": "after", + "frame": [ + 2, + 7, + 12, + 24, + 55, + 75, + 232, + 484 + ] + } + ], + "target_annotated_vectors": [ + 2, + 7, + 12, + 24, + 55, + 75, + 95, + 232, + 484, + 486 + ], + "basis_head_in_any_target_annotation": true, + "basis_head_in_source_after_drop": false, + "drop_after_span_decomposition_of_head": [ + 8, + 32, + 64, + 128 + ], + "drop_transport_span_nested": true, + "source_annotation_count": 22, + "source_annotations_span_hosting_basis_head": 22, + "source_span_drop_events": [], + "target_span_first_hosting_event": 3473, + "target_span_first_hosting_role": "after", + "target_preterminal_annotations_span_hosting_basis_head": 0, + "target_arrive_before_span": [ + 0, + 95, + 441, + 486 + ], + "target_update_events": [ + 19, + 20, + 2013, + 2146, + 2526, + 2797 + ], + "target_updates_in_head_free_span": 6, + "target_last_update_event": 2797, + "target_events_after_span_cohost_open": 0, + "source_events_after_span_cohost_open": [ + 3642, + 3798, + 3850, + 3954 + ], + "endpoint_transport_count": 8, + "endpoint_transports_span_nested_upward": true, + "endpoint_transport_rank_steps_match": true, + "targets_whose_final_contains_basis_head_among_all": 24, + "hit_flags_from_census": [ + 0, + 1, + 9, + 43 + ], + "flag_is_present_head_case": true, + "obstruction": "published_channel_hosts_basis_head_on_matched_target_only_at_terminal_transport_literally_and_in_span_after_every_target_update", + "no_new_kappa": true, + "selected_kappa": "0.001672660197076918" +} diff --git a/research/p104-present-head-flag1-audit/MASTER-HANDOFF.md b/research/p104-present-head-flag1-audit/MASTER-HANDOFF.md new file mode 100644 index 0000000000..5614ae8fda --- /dev/null +++ b/research/p104-present-head-flag1-audit/MASTER-HANDOFF.md @@ -0,0 +1,105 @@ +# Master handoff — `research/p104-present-head-flag1-audit/` + +## Candidate + +- Branch: `cursor/p104-present-head-flag1-60b9` (VictorLiwentao fork) +- Content tip: `112436d9be29b668c9306901843c440dafac3755` (scientific package + commit; parent is the pinned base) +- Packaging tip: the child commit that adds only this handoff file. Read its SHA + from `git rev-parse origin/cursor/p104-present-head-flag1-60b9`. +- Package: `research/p104-present-head-flag1-audit/` +- Base: CrocSwap main `6f100d4bb5083f8c35d96fd95a539811c62f245c` +- Card: `p104-side-correction` (refined), priority revision 6 +- κ: unchanged `0.001672660197076918` + +## Claim + +On published present-head flag 1 (`X0` → `Y7`, basis head `232`), the head +enters `Y7`'s frame, listed and in GF(2) span, only at `Y7`'s terminal transport +after-frame (event 3473). All six `Y7` adds (last one at event 2797) run in +head-free charts. `X0`'s literal drop at event 591 is a nested chart change that +keeps `232` in span (`8 ^ 32 ^ 64 ^ 128`). No `Y7` event occurs while both +endpoints host the head direction, so chronological dirty restoration cannot use +co-hosted basis-head geometry on this word. + +## Why flag 1 and not flag 43 + +The brief said to switch to flag 43 only if flag 1 reprinted flag 9's numbers. +It does not. Flag 1 has drop 591, arrive 3473 and gap 2882. Flag 9 has drop 500, +arrive 3489 and gap 2989. The target, the head and the frames also differ. Flag +43 (`X21` → `Y59`, head `15`, drop 570, arrive 3525) is uncertified and remains +available. + +## New checkable facts beyond #3443's method + +- Span-level hosting: zero source span drops (22 of 22 `X0` annotations span + `232`), and zero preterminal `Y7` span hosting (largest preterminal span + `{0, 95, 441, 486}`). +- Target-update chronology: 6 of 6 `Y7` row updates run in head-free charts, + and there are 0 `Y7` events after the head enters `Y7`'s span. +- Frame semantics check: all 8 endpoint transports are nested upward, and each + paid rank equals the rank increase. +- Literal facts mirroring #3443: `preterminal_hosting=0`, `drop_event=591`, + `arrive_event=3473`, `hosting_gap_events=2882`, zero joint events, both frames + unrestored. + +## Evidence commands + +```sh +python3.12 -I -B research/p104-present-head-flag1-audit/verify.py +python3.12 -I -O -Werror -B research/p104-present-head-flag1-audit/verify.py +python3.12 -I -O -Werror -B research/p104-present-head-flag1-audit/independent.py +python3.12 -I -O -Werror -B research/p104-present-head-flag1-audit/test_package.py +python3.12 -B scripts/research_package.py --package research/p104-present-head-flag1-audit +``` + +Expected markers: + +```text +PASS_P104_PRESENT_HEAD_FLAG1 flag=1 head=232 preterminal_hosting=0 preterminal_span_hosting=0 drop_event=591 arrive_event=3473 source_span_drops=0 head_free_target_updates=6/6 no_new_kappa +PASS_P104_PRESENT_HEAD_FLAG1_INDEPENDENT flag=1 head=232 preterminal_hosting=0 preterminal_span_hosting=0 drop_event=591 arrive_event=3473 source_span_drops=0 head_free_target_updates=6/6 no_new_kappa +PASS_P104_PRESENT_HEAD_FLAG1_TESTS groups=6 +PASS_REGISTERED_RESEARCH_PACKAGE research/p104-present-head-flag1-audit outcome=completed +``` + +## Closest priors + +- #3443 `p104-present-head-flag9-audit`: the method mirrored here, on flag 9 + (leave alone). +- #3349 `p104-channel-touch-restoration-audit`: names the present-head class + `(0, 1, 9, 43)`, including `(X0, Y7, 232)`. It does not give `Y7`'s + chronology. +- #3392 `p104-absent-head-flag2-audit`: the complementary absent-head case + (leave alone). +- Merged #3242 `p104-flag-channel-schedule`: already records `X0` first touched + at 591 on `[232]` and zero joint events for every matched pair. + +## Soft-overlap risks + +- Flag 1 shares source `X0` and head `232` with flag 0. So the source-side drop + event 591 is the same one #3242 records for flag 0. The flag-0 coefficient + cascade (#3363/#3365/#3371/#3372/#3412) is about coefficients and `Y34`. This + package recomputes no coefficient and says nothing about `Y34`. #3363's census + of relay deliveries over all 208 flags implicitly includes flag 1's delivery + coefficient. This package does not restate it. +- The span reading cuts against #3443's wording. A one-line check (`196 = 132 ^ + 64`, with both in the event-500 after-frame `[8, 64, 132, 260]`) suggests + flag 9's "source drop" is also only a chart change. Consider adding a limits + note to #3443 before publishing either package. This package does not certify + flag 9. +- Do not extend this to flags 0, 9 or 43 in the same PR without a new fact. + +## Open questions + +1. Can a changed schedule bring `232` into `Y7`'s span before the add at event + 2797, while `X0` is still live, and what does that add to the channel bill? + The common-chart rule means `D17`'s frame at that add must move too. +2. Do flags 9 and 43 show the same span pattern (the source keeps the head and + the target gains it only at its terminal transport)? If so, the present-head + obstruction is a target-side property. + +## Disposition note for master + +The worker produces a fork branch and package only. Do **not** open a CrocSwap +PR from this worker. Master decides publish or defer after independent +skeptical review. diff --git a/research/p104-present-head-flag1-audit/NOTICE.md b/research/p104-present-head-flag1-audit/NOTICE.md new file mode 100644 index 0000000000..02ff76da57 --- /dev/null +++ b/research/p104-present-head-flag1-audit/NOTICE.md @@ -0,0 +1,9 @@ +# Notice + +This package is a finite annotated-frame audit of one published P104 matched +flag, read both as listed frame vectors and as GF(2) spans. It does not modify +frozen upstream sources. + +Prepared by Wentao Li with substantial AI assistance. +Apache-2.0; predecessor notices and exact source pins are retained in +`SOURCES.json`. diff --git a/research/p104-present-head-flag1-audit/PROOF.md b/research/p104-present-head-flag1-audit/PROOF.md new file mode 100644 index 0000000000..ffdd40d80a --- /dev/null +++ b/research/p104-present-head-flag1-audit/PROOF.md @@ -0,0 +1,99 @@ +# Proof: present-head flag 1 late-only target hosting, literal and in span + +## Setup + +Pin CrocSwap main `6f100d4bb5083f8c35d96fd95a539811c62f245c`, the #2981 +208-flag matching (`research/p104-joint-unit-flags/CERTIFICATE.json`), and the +reviewed #1991 channel witness +(`research/p104-native-channel/inputs/LOWRANK-WITNESS.json`, 4,058 events). + +A register annotation is a transport before- or after-frame, or an add frame, +naming that register. The basis head of a matched flag is the first vector of its +basis. Open #3349 records that the target final contains that head for exactly +flags `(0, 1, 9, 43)`. This note audits flag 1. + +Labels are vectors in the nine-dimensional binary space, written as integers +below 512. `research/p104-native-channel/PROOF.md` §2 treats each frame as a +binary frame `W` with canonical chart `Gamma_W`, and says every transport is +nested. A register *lists* the head when the head is one of the frame's vectors. +It *spans* the head when the head is a GF(2) sum of frame vectors. Listing +depends on the chosen generators. Spanning does not. + +## Statement + +Flag 1 has source `X0`, target `Y7` and basis head `232`. On the published word: + +1. `X0` begins at `[232]`. Its first event, transport 591, goes from `[232]` to + `[8, 32, 64, 128, 256]`. This removes `232` from the list. No later `X0` + annotation lists `232`. +2. The event-591 after-frame spans `232` through the unique decomposition + `8 ^ 32 ^ 64 ^ 128`. All 22 `X0` annotations span `232`. In span, the source + never drops the head. +3. `Y7` starts empty. Its preterminal frames are `[]`, `[95]` and `[95, 486]`. + Their spans exclude `232`; the largest is `{0, 95, 441, 486}`. +4. Event 3473 is the last `Y7` event. It is a transport from `[95, 486]` to the + target final `[2, 7, 12, 24, 55, 75, 232, 484]`. This after-frame is the first + `Y7` annotation that lists or spans `232`. The literal gap from the source + drop is 2,882 events. +5. `Y7`'s row changes only at adds with `Y7` as the destination: events 19, 20, + 2013, 2146, 2526 and 2797. Each add runs in a common chart that excludes + `232` from its span. +6. No event names both `X0` and `Y7`. `X0` has four events after 3473 (3642, + 3798, 3850 and 3954), and none of them names `Y7`. +7. All eight endpoint transports (five on `X0`, three on `Y7`) are nested upward. + Each transport's paid rank (its fifth field, which + `research/p104-native-channel/check_native.py` binds to the compiled recipe + rank) equals the rank increase. This matches the binary-frame reading. +8. Neither endpoint frame returns to its initial frame. `X0` goes from rank 1 to + rank 9 and `Y7` from rank 0 to rank 8. + +By items 2 and 4, the first chronological cut at which both endpoint frames +host the head direction is the after-frame of event 3473. By items 4 to 6, the +published word has no `Y7` event after that cut and no `Y7` update at or after +it. So no target update, and no event touching the target, happens while both +endpoints host the basis-head direction. Logical dirty restoration of the source +line into `Y7` along co-hosted basis-head geometry is unavailable on this word. +Under listing alone the same conclusion holds with a 2,882-event gap, as in the +#3443 method. + +## Checking method + +Two scanners read the same pinned inputs. The primary scanner walks annotations +in program order and decides span membership by pivot-indexed row reduction. It +tracks combinations so it can return the decomposition of the head. The second +scanner indexes events per endpoint first, then builds each span as an explicit +XOR closure (at most 512 labels) and finds the decomposition by exhaustive subset +search. Both reject duplicate JSON keys and dependent frames, enforce the +SHA-256 source pins, and admit through `need()` under `python -O`. Their +receipts must equal the committed certificate. + +`test_package.py` copies the package and its inputs into a temporary tree. It +mutates four certificate fields, injects a duplicate key and flips one byte of +the witness. Both scanners must reject each change under `-O`. A negative +control edits an in-memory witness so that `Y7`'s frame from event 2796 onward +is `[95, 95 ^ 232]`, which spans `232` without listing it. The listing count +stays at zero, but the span fields move: hosting starts at 2796 and one of the +six adds now runs in a head-hosting chart. This shows the span check catches +what listing misses. + +## Soft overlap + +Merged #3242 already records `X0`'s first event at 591 on `[232]`, and that no +matched pair shares an event. This package reuses those facts and adds the span +reading of the source and the target-side chronology for `Y7`. Open +#3363/#3365/#3371/#3372 record coefficient delivery for the +channel/relay/Gram/tail path, worked on flag 0, which shares source `X0` with +flag 1. This package recomputes no coefficient and makes no claim about `Y34`. +Open #3443 states flag 9's drop as literal membership. Item 2 shows that for +flag 1 a literal drop is a chart change, not a loss of direction. This package +does not re-audit flag 9. Open #3392 (flag 2) and the #3349 census are not +recomputed. + +## Limits + +This is a statement about the published frames of one matched flag. "Hosting" +means the head is listed in, or spanned by, an annotated endpoint frame. The +package does not model what the head direction means inside the relay registers +(`G`, `Q`, `D`, `C`). It does not price a repair, construct a changed schedule, +or claim a new κ. A schedule that brings `232` into `Y7`'s span before event +2797 is outside this certificate. diff --git a/research/p104-present-head-flag1-audit/README.md b/research/p104-present-head-flag1-audit/README.md new file mode 100644 index 0000000000..48e105431a --- /dev/null +++ b/research/p104-present-head-flag1-audit/README.md @@ -0,0 +1,63 @@ +# Present-head flag 1: the basis head reaches the target only after its last update + +**Scoped obstruction. No new exponent.** + +Open [#3349](https://github.com/CrocSwap/integer-mult-bounds/pull/3349) shows the +basis head is in the target final on only four of the 208 matched flags: +`(0, 1, 9, 43)`. Open [#3443](https://github.com/CrocSwap/integer-mult-bounds/pull/3443) +pins flag 9. This package pins flag 1 (`X0` → `Y7`, basis head `232`). + +On the published 4,058-event word, `Y7` holds `[]`, `[95]` and `[95, 486]` before +its last event. None of these lists `232`, and none spans it over GF(2). The head +enters `Y7` only in the after-frame of the terminal transport at event 3473. All +six adds into `Y7` (events 19 through 2797) run in charts that exclude the head +direction. No event names both `X0` and `Y7`, and neither frame is restored. + +The source side behaves differently from what a literal reading suggests. `X0` +starts at `[232]`, and its first transport (event 591) lists +`[8, 32, 64, 128, 256]`. That drops `232` from the list but not from the span, +because `232 = 8 ^ 32 ^ 64 ^ 128`. Every one of the 22 `X0` annotations spans the +head. The native channel's frames are binary subspaces with nested transports, so +the span reading is the chart-independent one. + +Both endpoints first host the head direction together at event 3473, and `Y7` has +no event after that. The published channel therefore never updates or touches the +matched target while both endpoints host the basis-head direction. Chronological +dirty restoration along co-hosted basis-head geometry is unavailable on this +word. In span, the obstruction is entirely on the target side. + +Selected κ stays 0.001672660197076918. Details and limits are in +[PROOF.md](PROOF.md). + +## Reproduce + +```sh +python3.12 -I -B research/p104-present-head-flag1-audit/verify.py +python3.12 -I -O -Werror -B research/p104-present-head-flag1-audit/verify.py +python3.12 -I -O -Werror -B research/p104-present-head-flag1-audit/independent.py +python3.12 -I -O -Werror -B research/p104-present-head-flag1-audit/test_package.py +python3.12 -B scripts/research_package.py --package research/p104-present-head-flag1-audit +``` + +`verify.py` is read-only. Admission goes through `need()` and still fires under +`-O`. `test_package.py` corrupts temporary copies of the certificate and of one +pinned input and checks that both scanners reject them under `-O`. + +## Credit + +Credit Nick Petalas / #2981 for the flag matching, the reviewed #1991 channel +lineage for the witness, jwr404 / #3242 for the schedule receipt, #3349 for the +present-head census, #3443 for the flag-9 method, and #3392 for the absent-head +counterpart. Prepared by Wentao Li with substantial AI assistance. + +## Open next questions + +1. Can a changed schedule put `232` into `Y7`'s span before its last add (event + 2797) while `X0` is still live, and what does that cost against the channel + bill? +2. Do flags 9 and 43 follow the same pattern in span, with the source keeping the + head direction and the target gaining it only at its terminal transport? If + so, #3443's literal source drop is a chart change, and the present-head + obstruction is a target-side property. + +[TASK.json](TASK.json) gives first steps and blockers for both. diff --git a/research/p104-present-head-flag1-audit/SOURCES.json b/research/p104-present-head-flag1-audit/SOURCES.json new file mode 100644 index 0000000000..6442bdd68a --- /dev/null +++ b/research/p104-present-head-flag1-audit/SOURCES.json @@ -0,0 +1,44 @@ +{ + "schema_version": 1, + "base_commit": "6f100d4bb5083f8c35d96fd95a539811c62f245c", + "upstream": "CrocSwap/integer-mult-bounds", + "files": [ + { + "path": "research/p104-joint-unit-flags/CERTIFICATE.json", + "usage": "input", + "git_blob": "0fa7d2d40566e92f3ea1539723abf438ba65adb8", + "sha256": "a98126428a8da6eae91c50afcc42e014a284c82b554ef77e5b3a34fc6d228128", + "credit": "Nick Petalas, PR #2981" + }, + { + "path": "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "usage": "input", + "git_blob": "86beaf424e9f0f800ae3a62797d94ec9386b7706", + "sha256": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e", + "credit": "Reviewed #1991 native channel witness" + }, + { + "path": "research/p104-endpoint-geometric-budget/geometry.py", + "usage": "input", + "git_blob": "f49752bcfc321a6129186d4daa774b2c3fdb84f1", + "sha256": "1a2792189beaf15aa8180136ca007cd2301992a62e77ba72edea99b298e4148f", + "credit": "X/Y naming lines for the 104 sources and 104 targets" + }, + { + "path": "research/p104-native-channel/PROOF.md", + "usage": "provenance", + "git_blob": "a69311b74f74a2f8e8f411c1451baacd9bacddce", + "sha256": "5d743145d389ffdfaffc66096fa7e32c7155b18f73d74755403151d0435bb94c", + "pin": "base_commit:research/p104-native-channel/PROOF.md", + "credit": "Binary-frame semantics: nine-dimensional binary label space and nested transports" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0", + "pin": "base_commit:docs/research/agent-task-catalog.json", + "credit": "Priority revision 6 task catalogue at the pinned base" + } + ] +} diff --git a/research/p104-present-head-flag1-audit/TASK.json b/research/p104-present-head-flag1-audit/TASK.json new file mode 100644 index 0000000000..2d1b7ef979 --- /dev/null +++ b/research/p104-present-head-flag1-audit/TASK.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 6, + "selected_kappa": "0.001672660197076918", + "base_commit": "6f100d4bb5083f8c35d96fd95a539811c62f245c", + "original_card": { + "id": "p104-side-correction", + "question": "Can the proposed P104 joint endpoint flags be realized by a chronological correction program with coefficients, dirty restoration and an affordable complete bill?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/p104-native-channel/README.md", + "research/p104-native-channel/PROOF.md", + "docs/research/community-efficient1000-review.md", + "research/p104-joint-unit-flags/README.md" + ], + "methods": [ + "Construct one side-correction word at an explicit chronological cut with the needed frames still available.", + "Derive a lower bound on the side correction and hosting costs that decides whether this channel can beat the selected budget." + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the revision-6 family record and #2981 static joint flags, alongside the reviewed #1991 channel. #2981 is an author-checked source archive, not an independently validated executable correction or a refutation of program-level lifetime floors.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "After checking live handoffs, pin one named collection from #2981 and attach acquisition/delivery times, source dependencies and coefficient requirements. Test legal access and arbitrary dirty restoration; price any completion against the full channel/endpoint/hosting allowance. Stop with the exact missing implication or a scoped counterexample rather than expanding the static cover census.", + "bottleneck_link": "Completing an already realized changed channel tests a concrete construction opportunity, instead of refining the incumbent packing. A positive local result still needs global and all-size admission.", + "allowed_variations": [ + "One correction factorization, one chronological cut, or one explicit hosting obstruction.", + "A changed correction schedule with an updated full bill and native frame contract." + ], + "scope_change_triggers": [ + "Recompiling the already certified low-rank channel without closing a new obligation.", + "Treating a pending ancestor, local histogram or unpriced side correction as an admitted global supplier.", + "Repeating a correction or physical conversion already supplied by a pending follow-up without adding independent coverage or a different unresolved obligation.", + "Repeating the 208-flag static matching or calling a static nested cover a chronological correction program. Independent audit of that certificate is distinct and remains useful." + ], + "overlap_terms": [ + "P104", + "I-G/2", + "side correction", + "native channel", + "1972", + "1991", + "2586", + "endpoint transport", + "physical dual", + "relay composition", + "2981", + "joint unit flags", + "acquisition delivery", + "static nesting" + ], + "existing_checks": [ + { + "scope": "PR #2981 reports static joint endpoint flags and a matching of 208 departure and arrival flags; archival intake is not independent verification.", + "evidence": "research/p104-joint-unit-flags/README.md", + "remaining": "Independent flag check and a chronological coefficient program with dirty restoration and a complete cost.", + "status": "author-checked", + "source_commit": "3d24b92d8ba057b57cb2d480170ec407520e6882", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Pin matched present-head flag 1 (X0 to Y7, basis head 232) from the #2981 certificate and prove on the published #1991 channel that the basis head enters Y7's frame, both as a listed vector and in the GF(2) span, only at Y7's terminal transport after-frame (event 3473), after all six Y7 row updates have run in head-free charts, while X0's span keeps the head at every annotation. No Y7 event occurs while both endpoint frames host the head direction, so chronological dirty restoration cannot use co-hosted basis-head geometry on this word.", + "scope_change_reason": "Open #3349 registers the 208-flag restoration census and names the present-head class (0, 1, 9, 43). Open #3443 pins flag 9 with literal frame membership. Open #3392 pins absent-head flag 2. Open #3363/#3365/#3371/#3372 cover algebraic coefficient delivery concentrated on flag 0. Flag 1 is the next present-head member outside those packages. Its numbers differ from flag 9 (drop 591, arrive 3473, gap 2882), so it is not a reprint. Because the native channel's frames are binary subspaces with nested transports, this package also checks hosting in span: the literal source drop is a chart change, and the obstruction is entirely on the target side.", + "bottleneck_link": "A present-head target final does not host the basis-head direction while the target is still being updated. On flag 1 every Y7 row update precedes the head's entry into Y7's span, and Y7 has no event after that entry, so a dirty restoration using co-hosted geometry needs new target events.", + "budget_minutes": 60, + "stop_rule": "Stop after flag 1's late-only hosting obstruction is pinned literally and in span and dual-scanned. Do not build a correction word, recompute algebraic relays, or certify flags 0, 9 or 43.", + "outcome": "completed", + "evidence": "Flag 1 is source 0, target 7, basis head 232. X0 starts at [232]; its first transport at event 591 goes to [8, 32, 64, 128, 256], removing 232 from the list but not from the span (232 = 8 xor 32 xor 64 xor 128). All 22 X0 annotations span the head. Y7's preterminal frames are [], [95] and [95, 486], whose spans exclude 232. The head enters Y7 only in the after-frame of event 3473, Y7's last event (literal gap 2882 after event 591). Y7's six adds (events 19, 20, 2013, 2146, 2526, 2797) all run in head-free charts. No joint X0/Y7 event exists; all eight endpoint transports are nested upward with rank steps equal to their recorded costs. Neither endpoint frame is restored (ranks 1 to 9 and 0 to 8). Selected kappa is unchanged.", + "author": "Wentao Li", + "ai_assistance": "Substantial AI assistance for derivation, implementation, checking and writing.", + "no_new_kappa": true, + "open_questions": [ + { + "question": "Can a changed schedule place 232 in Y7's span before Y7's last row update, while X0 is still live, and what does that add to the channel bill?", + "why_it_matters": "On the published word the head direction reaches Y7 only at its final transport, after the last add at event 2797. A repair must move a rank step of Y7 earlier or add target events, and both cost transports.", + "first_step": "Try moving part of Y7's rank-six terminal step (event 3473) ahead of the add at event 2797 so that 232 is in span there. Then check the common-chart requirement against D17's frame at that add.", + "blocked_by": "This package reads only the published frames of flag 1. It does not construct a repair, price one, or check D17's frame contract." + }, + { + "question": "Do the other present-head flags show the same pattern in span: the source keeps the head direction throughout and the target gains it only at its terminal transport?", + "why_it_matters": "Open #3443 states flag 9's source drop as literal membership. If spans behave as they do on flag 1, the present-head obstruction is a target-side property, and a changed schedule only needs earlier target hosting.", + "first_step": "Rerun this package's span check on flags 9 and 43 against the same pinned inputs. Do not touch flag 0, which belongs to the coefficient cascade.", + "blocked_by": "This package certifies flag 1 only. Flag 9 is the subject of open #3443." + } + ] +} diff --git a/research/p104-present-head-flag1-audit/VERIFY.json b/research/p104-present-head-flag1-audit/VERIFY.json new file mode 100644 index 0000000000..f5b206c110 --- /dev/null +++ b/research/p104-present-head-flag1-audit/VERIFY.json @@ -0,0 +1,28 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-joint-unit-flags/CERTIFICATE.json", + "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "research/p104-endpoint-geometric-budget/geometry.py" + ], + "commands": [ + { + "argv": ["{python}", "-I", "-O", "-Werror", "-B", "{package}/verify.py"], + "timeout_seconds": 60, + "checks": "Program-order scan of flag 1 hosting on X0 and Y7: literal frames plus GF(2) span by row reduction" + }, + { + "argv": ["{python}", "-I", "-O", "-Werror", "-B", "{package}/independent.py"], + "timeout_seconds": 60, + "checks": "Per-register scan of the same flag-1 obstruction with explicit XOR-closure spans and subset search" + }, + { + "argv": ["{python}", "-I", "-O", "-Werror", "-B", "{package}/test_package.py"], + "timeout_seconds": 120, + "checks": "Duplicate JSON keys, temp-tree certificate and input corruption under -O, optimized admission, span negative control, scanner agreement, read-only replay" + } + ] +} diff --git a/research/p104-present-head-flag1-audit/independent.py b/research/p104-present-head-flag1-audit/independent.py new file mode 100644 index 0000000000..143c0d6626 --- /dev/null +++ b/research/p104-present-head-flag1-audit/independent.py @@ -0,0 +1,343 @@ +#!/usr/bin/env python3 +"""Second flag-1 present-head scanner. It does not import verify.py. + +Events are first indexed per endpoint register. Literal frames are frozensets; +spans are explicit XOR closures (at most 512 labels), so membership, rank and +nesting are set operations rather than row reduction. The head decomposition +is found by exhaustive subset search. Admission uses need() under -O. +""" + +import hashlib +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +MARKER = ( + "PASS_P104_PRESENT_HEAD_FLAG1_INDEPENDENT flag=1 head=232 " + "preterminal_hosting=0 preterminal_span_hosting=0 drop_event=591 " + "arrive_event=3473 source_span_drops=0 head_free_target_updates=6/6 " + "no_new_kappa" +) +INPUTS = ( + "research/p104-joint-unit-flags/CERTIFICATE.json", + "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "research/p104-endpoint-geometric-budget/geometry.py", +) +SOURCE_LINE = "sources = [paths[f'X{s}'] for s in range(104)]" +TARGET_LINE = "targets = [paths[f'Y{t}'] for t in range(104)]" +FLAG_INDEX = 1 +HIT_FLAGS = (0, 1, 9, 43) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def pairs_unique(pairs): + value = {} + for key, item in pairs: + need(key not in value, "duplicate JSON key") + value[key] = item + return value + + +def read_json(path): + raw = Path(path).read_bytes() + need(len(raw) <= 2_000_000, "input exceeds 2 MB") + return json.loads(raw, object_pairs_hook=pairs_unique) + + +def frame_set(frame): + need(type(frame) is list, "frame") + values = [] + for entry in frame: + need(type(entry) is int and 0 < entry < 512, "frame entry") + values.append(entry) + folded = frozenset(values) + need(len(folded) == len(values), "duplicate frame vector") + return folded + + +def closure(frame): + """Explicit GF(2) span of an independent frame.""" + span = {0} + for vector in frame_set(frame): + span = span | {vector ^ old for old in span} + need(len(span) == 1 << len(frame), "dependent frame") + return frozenset(span) + + +def dimension(frame): + return len(closure(frame)).bit_length() - 1 + + +def subset_xor(vector, frame): + found = [] + for mask in range(1 << len(frame)): + acc = 0 + chosen = [] + for position, entry in enumerate(frame): + if mask & (1 << position): + acc ^= entry + chosen.append(entry) + if acc == vector: + found.append(sorted(chosen)) + need(len(found) <= 1, "non-unique decomposition") + return found[0] if found else None + + +def index_registers(program, wanted): + table = {name: [] for name in wanted} + joint = 0 + for index, event in enumerate(program): + need(type(event) is list and 1 <= len(event) <= 8, "event shape") + present = {item for item in event if type(item) is str and item in table} + if len(present) == len(table): + joint += 1 + for name in present: + table[name].append(index) + return table, joint + + +def frames_of(event, name): + if event[0] == "transport" and event[1] == name: + return [("before", event[2]), ("after", event[3])] + if event[0] == "add" and name in (event[1], event[2]): + return [("add", event[-1])] + return [] + + +def pin_sources(): + manifest = read_json(HERE / "SOURCES.json") + rows = [row for row in manifest["files"] if row["usage"] == "input"] + need(tuple(row["path"] for row in rows) == INPUTS, "input inventory") + pinned = {} + for row in rows: + raw = (ROOT / row["path"]).read_bytes() + need(hashlib.sha256(raw).hexdigest() == row["sha256"], "source hash: " + row["path"]) + pinned[row["path"]] = raw + return pinned + + +def evaluate(): + pinned = pin_sources() + geometry = pinned[ + "research/p104-endpoint-geometric-budget/geometry.py" + ].decode("utf-8") + need(SOURCE_LINE in geometry and TARGET_LINE in geometry, "geometry naming") + helpers = json.loads( + pinned["research/p104-joint-unit-flags/CERTIFICATE.json"], + object_pairs_hook=pairs_unique, + )["helpers"] + witness = json.loads( + pinned["research/p104-native-channel/inputs/LOWRANK-WITNESS.json"], + object_pairs_hook=pairs_unique, + ) + program = witness["program"] + need(len(helpers) == 208 and len(program) == 4058, "sizes") + hits = [ + index + for index, row in enumerate(helpers) + if row["basis"][0] in witness["final_frames"][f"Y{row['target']}"] + ] + need(hits == list(HIT_FLAGS), "hit-flag census drift") + need(FLAG_INDEX in hits, "flag 1 left the present-head class") + helper = helpers[FLAG_INDEX] + head = helper["basis"][0] + source = f"X{helper['source']}" + target = f"Y{helper['target']}" + table, joint = index_registers(program, (source, target)) + source_indices = table[source] + target_indices = table[target] + need(source_indices and target_indices, "endpoint silence") + + source_hits = [] + source_frames = 0 + source_span_frames = 0 + source_span_drops = [] + transports = [] + for index in source_indices: + event = program[index] + if event[0] == "transport" and event[1] == source: + transports.append(event) + for role, frame in frames_of(event, source): + literal = frame_set(frame) + source_frames += 1 + if head in closure(frame): + source_span_frames += 1 + else: + source_span_drops.append(index) + if head in literal: + source_hits.append( + { + "event": index, + "opcode": event[0], + "role": role, + "frame": sorted(literal), + } + ) + + target_hits = [] + target_span_hits = [] + target_pool = set() + updates = [] + head_free_updates = 0 + for index in target_indices: + event = program[index] + if event[0] == "transport" and event[1] == target: + transports.append(event) + if event[0] == "add" and event[1] == target: + updates.append(index) + if head not in closure(event[-1]): + head_free_updates += 1 + for role, frame in frames_of(event, target): + literal = frame_set(frame) + target_pool |= literal + if head in closure(frame): + target_span_hits.append((index, role)) + if head in literal: + target_hits.append( + { + "event": index, + "opcode": event[0], + "role": role, + "frame": sorted(literal), + } + ) + + drop = source_indices[0] + drop_event = program[drop] + need(drop_event[0] == "transport" and drop_event[1] == source, "first source op") + drop_before = sorted(frame_set(drop_event[2])) + drop_after = sorted(frame_set(drop_event[3])) + need(drop_before == [head], "drop before") + need(head not in drop_after, "drop after") + need(len(target_hits) == 1, "unexpected target head hosting count") + arrive = target_hits[0] + need(arrive["opcode"] == "transport" and arrive["role"] == "after", "arrive shape") + need(arrive["event"] == target_indices[-1], "arrive not terminal") + arrive_event = program[arrive["event"]] + arrive_before = sorted(frame_set(arrive_event[2])) + arrive_after = sorted(frame_set(arrive_event[3])) + need(head not in arrive_before and head in arrive_after, "arrive frames") + preterminal = [row for row in target_hits if row["event"] < arrive["event"]] + need(target_span_hits, "no span hosting on target") + span_open, span_role = target_span_hits[0] + span_preterminal = [row for row in target_span_hits if row[0] < arrive["event"]] + after_drop = any( + row["event"] > drop or (row["event"] == drop and row["role"] == "after") + for row in source_hits + ) + nested = all(closure(event[2]) <= closure(event[3]) for event in transports) + steps = all( + event[4] == dimension(event[3]) - dimension(event[2]) for event in transports + ) + source_initial = witness["initial_frames"][source] + source_final = witness["final_frames"][source] + target_initial = witness["initial_frames"][target] + target_final = witness["final_frames"][target] + finals_with_head = len( + [name for name, frame in witness["final_frames"].items() + if name.startswith("Y") and head in frame] + ) + receipt = { + "schema_version": 1, + "claim_id": "p104-present-head-flag1-audit", + "pinned_main": "6f100d4bb5083f8c35d96fd95a539811c62f245c", + "flag_index": FLAG_INDEX, + "source": helper["source"], + "target": helper["target"], + "basis_head": head, + "departure_choice": helper["departure_choice"], + "arrival_choice": helper["arrival_choice"], + "basis": helper["basis"], + "source_register": source, + "target_register": target, + "source_initial": source_initial, + "source_final": source_final, + "target_initial": target_initial, + "target_final": target_final, + "source_initial_is_basis_head": source_initial == [head], + "target_final_contains_basis_head": head in target_final, + "source_frame_restored": frame_set(source_initial) == frame_set(source_final), + "target_frame_restored": frame_set(target_initial) == frame_set(target_final), + "source_rank_initial": dimension(source_initial), + "source_rank_final": dimension(source_final), + "target_rank_initial": dimension(target_initial), + "target_rank_final": dimension(target_final), + "source_first_event": source_indices[0], + "source_last_event": source_indices[-1], + "target_first_event": target_indices[0], + "target_last_event": target_indices[-1], + "source_event_count": len(source_indices), + "target_event_count": len(target_indices), + "joint_source_target_events": joint, + "basis_head_drop_event": drop, + "basis_head_drop_before": drop_before, + "basis_head_drop_after": drop_after, + "basis_head_arrive_event": arrive["event"], + "basis_head_arrive_before": arrive_before, + "basis_head_arrive_after": arrive_after, + "hosting_gap_events": arrive["event"] - drop, + "source_annotations_containing_basis_head": len(source_hits), + "target_annotations_containing_basis_head": len(target_hits), + "target_preterminal_annotations_containing_basis_head": len(preterminal), + "source_head_annotations": source_hits, + "target_head_annotations": target_hits, + "target_annotated_vectors": sorted(target_pool), + "basis_head_in_any_target_annotation": head in target_pool, + "basis_head_in_source_after_drop": after_drop, + "drop_after_span_decomposition_of_head": subset_xor(head, drop_event[3]), + "drop_transport_span_nested": closure(drop_event[2]) <= closure(drop_event[3]), + "source_annotation_count": source_frames, + "source_annotations_span_hosting_basis_head": source_span_frames, + "source_span_drop_events": source_span_drops, + "target_span_first_hosting_event": span_open, + "target_span_first_hosting_role": span_role, + "target_preterminal_annotations_span_hosting_basis_head": len(span_preterminal), + "target_arrive_before_span": sorted(closure(arrive_event[2])), + "target_update_events": updates, + "target_updates_in_head_free_span": head_free_updates, + "target_last_update_event": updates[-1], + "target_events_after_span_cohost_open": len( + [index for index in target_indices if index > span_open] + ), + "source_events_after_span_cohost_open": [ + index for index in source_indices if index > span_open + ], + "endpoint_transport_count": len(transports), + "endpoint_transports_span_nested_upward": nested, + "endpoint_transport_rank_steps_match": steps, + "targets_whose_final_contains_basis_head_among_all": finals_with_head, + "hit_flags_from_census": list(HIT_FLAGS), + "flag_is_present_head_case": True, + "obstruction": ( + "published_channel_hosts_basis_head_on_matched_target_only_at_" + "terminal_transport_literally_and_in_span_after_every_target_update" + ), + "no_new_kappa": True, + "selected_kappa": "0.001672660197076918", + } + need(receipt["target_final_contains_basis_head"] is True, "left present-head class") + need(receipt["target_preterminal_annotations_containing_basis_head"] == 0, "preterminal") + need(receipt["target_preterminal_annotations_span_hosting_basis_head"] == 0, "span preterminal") + need(receipt["source_span_drop_events"] == [], "source lost head direction") + need(receipt["target_updates_in_head_free_span"] == len(updates), "head-hosting update") + need(receipt["target_events_after_span_cohost_open"] == 0, "target event after cohost") + need(receipt["basis_head_in_source_after_drop"] is False, "source relisted head") + need(receipt["joint_source_target_events"] == 0, "joint endpoint event") + need(nested and steps, "transport semantics") + return receipt + + +def main(): + observed = evaluate() + expected = read_json(HERE / "CERTIFICATE.json") + need(observed == expected, "certificate mismatch") + print(MARKER) + + +if __name__ == "__main__": + main() diff --git a/research/p104-present-head-flag1-audit/test_package.py b/research/p104-present-head-flag1-audit/test_package.py new file mode 100644 index 0000000000..27ed034e7b --- /dev/null +++ b/research/p104-present-head-flag1-audit/test_package.py @@ -0,0 +1,217 @@ +#!/usr/bin/env python3 +"""Admission, corruption, span-control and scanner-agreement checks. No asserts.""" + +import copy +import hashlib +import json +import shutil +import subprocess +import sys +import tempfile +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +import independent +import verify + +SLUG = "research/" + HERE.name + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def tree_digest(paths): + return { + str(path): hashlib.sha256(path.read_bytes()).hexdigest() for path in paths + } + + +def watched_files(): + files = [path for path in HERE.iterdir() if path.is_file()] + files.extend(ROOT / name for name in verify.INPUTS) + return sorted(files) + + +def test_duplicate_key(): + with tempfile.TemporaryDirectory() as tmp: + path = Path(tmp) / "dup.json" + path.write_text('{"a": 1, "a": 2}\n', encoding="utf-8") + for reader in (verify.read_json, independent.read_json): + try: + reader(path) + except ValueError as exc: + need(str(exc) == "duplicate JSON key", "duplicate message") + else: + need(False, "duplicate key accepted") + + +def stage_tree(tmp): + """Copy the package and its pinned inputs into a throwaway repository root.""" + root = Path(tmp) + for name in verify.INPUTS: + destination = root / name + destination.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / name, destination) + package = root / SLUG + package.mkdir(parents=True) + for path in HERE.iterdir(): + if path.is_file() and path.suffix in (".py", ".json"): + shutil.copyfile(path, package / path.name) + return root, package + + +def run_optimized(script): + return subprocess.run( + [sys.executable, "-I", "-O", "-B", str(script)], + check=False, + capture_output=True, + text=True, + timeout=60, + ) + + +def expect_rejection(script, needle): + done = run_optimized(script) + need(done.returncode != 0, "corruption accepted: " + script.name) + need(needle in done.stderr, "wrong rejection for " + script.name + ": " + done.stderr[-200:]) + + +def test_temp_copy_corruption(): + before = tree_digest(watched_files()) + with tempfile.TemporaryDirectory() as tmp: + root, package = stage_tree(tmp) + for name in ("verify.py", "independent.py"): + done = run_optimized(package / name) + need(done.returncode == 0, "clean temp copy failed: " + done.stderr[-200:]) + cert = package / "CERTIFICATE.json" + clean = cert.read_bytes() + mutations = ( + ("basis_head_drop_event", 0), + ("target_span_first_hosting_event", 2797), + ("source_span_drop_events", [591]), + ("target_updates_in_head_free_span", 5), + ) + for key, value in mutations: + blob = json.loads(clean) + blob[key] = value + cert.write_text(json.dumps(blob, indent=2) + "\n", encoding="utf-8") + expect_rejection(package / "verify.py", "certificate mismatch") + expect_rejection(package / "independent.py", "certificate mismatch") + text = clean.decode("utf-8").replace( + '"schema_version": 1,', '"schema_version": 1,\n "schema_version": 1,', 1 + ) + cert.write_text(text, encoding="utf-8") + expect_rejection(package / "verify.py", "duplicate JSON key") + expect_rejection(package / "independent.py", "duplicate JSON key") + cert.write_bytes(clean) + witness = root / verify.INPUTS[1] + raw = bytearray(witness.read_bytes()) + position = raw.index(b"232") + raw[position:position + 3] = b"233" + witness.write_bytes(bytes(raw)) + expect_rejection(package / "verify.py", "source hash") + expect_rejection(package / "independent.py", "source hash") + need(tree_digest(watched_files()) == before, "live files mutated by corruption test") + + +def test_optimized_admission(): + script = ( + "import sys\n" + f"sys.path.insert(0, {str(HERE)!r})\n" + "import verify, independent\n" + "verify.need(__debug__ is False, 'optimization off')\n" + "for module in (verify, independent):\n" + " try:\n" + " module.need(False, 'admission')\n" + " except ValueError as exc:\n" + " if str(exc) != 'admission':\n" + " raise SystemExit('wrong admission')\n" + " else:\n" + " raise SystemExit('admission skipped')\n" + "print('PASS_OPTIMIZED_ADMISSION')\n" + ) + done = subprocess.run( + [sys.executable, "-O", "-I", "-B", "-c", script], + check=False, + capture_output=True, + text=True, + timeout=60, + ) + need(done.returncode == 0, "optimized admission failed: " + done.stderr) + need("PASS_OPTIMIZED_ADMISSION" in done.stdout, "optimized marker") + + +def test_sample_span_geometry(): + drop = ["transport", "X0", [232], [8, 32, 64, 128, 256], 4] + frames = verify.annotated_frames(drop, "X0") + need(frames[0] == ("before", [232]), "sample before") + need(232 not in frames[1][1], "sample literal drop") + need(verify.span_combination(232, drop[3]) == [8, 32, 64, 128], "primary decomposition") + need(independent.subset_xor(232, drop[3]) == [8, 32, 64, 128], "subset decomposition") + need(8 ^ 32 ^ 64 ^ 128 == 232, "head arithmetic") + need(verify.span_contains(drop[3], drop[2]), "primary nesting") + need(independent.closure(drop[2]) <= independent.closure(drop[3]), "closure nesting") + need(verify.rank(drop[3]) - verify.rank(drop[2]) == drop[4], "rank step") + late = [95, 486] + need(not verify.in_span(232, late), "primary late span") + need(232 not in independent.closure(late), "closure late span") + need(verify.span_elements(late) == [0, 95, 441, 486], "late span elements") + need(sorted(independent.closure(late)) == [0, 95, 441, 486], "late closure elements") + for bad in ([232, 232], [8, 32, 40]): + for check in (verify.rank, independent.dimension): + try: + check(bad) + except ValueError: + pass + else: + need(False, "dependent frame accepted") + + +def test_span_negative_control(): + pinned = verify.pin_sources() + helpers = json.loads(pinned[verify.INPUTS[0]])["helpers"] + witness = json.loads(pinned[verify.INPUTS[1]]) + clean = verify.build_receipt(witness, helpers) + need(clean["target_updates_in_head_free_span"] == 6, "clean update count") + mutated = copy.deepcopy(witness) + program = mutated["program"] + need(program[2796][:2] == ["transport", "Y7"] and program[2796][3] == [95, 486], "anchor 2796") + need(program[2797][:3] == ["add", "Y7", "D17"], "anchor 2797") + hosted = [95, 232 ^ 95] + program[2796][3] = list(hosted) + program[2797][-1] = list(hosted) + program[3473][2] = list(hosted) + shifted = verify.build_receipt(mutated, helpers) + need(shifted["target_preterminal_annotations_containing_basis_head"] == 0, "literal blind") + need(shifted["target_preterminal_annotations_span_hosting_basis_head"] == 2, "span sees head") + need(232 in shifted["target_arrive_before_span"], "arrive before now hosts head") + need(shifted["target_span_first_hosting_event"] == 2796, "span arrive moved") + need(shifted["target_updates_in_head_free_span"] == 5, "update now hosts head") + need(shifted != clean, "control did not change receipt") + + +def test_scanners_agree(): + before = tree_digest(watched_files()) + left = verify.evaluate() + right = independent.evaluate() + need(left == right, "scanner disagreement") + verify.admit(left, verify.read_json(HERE / "CERTIFICATE.json")) + need(tree_digest(watched_files()) == before, "package or input files mutated") + + +def main(): + test_duplicate_key() + test_temp_copy_corruption() + test_optimized_admission() + test_sample_span_geometry() + test_span_negative_control() + test_scanners_agree() + print("PASS_P104_PRESENT_HEAD_FLAG1_TESTS groups=6") + + +if __name__ == "__main__": + main() diff --git a/research/p104-present-head-flag1-audit/verify.py b/research/p104-present-head-flag1-audit/verify.py new file mode 100644 index 0000000000..3a1219373a --- /dev/null +++ b/research/p104-present-head-flag1-audit/verify.py @@ -0,0 +1,415 @@ +#!/usr/bin/env python3 +"""Read-only present-head dirty-restoration audit for matched flag 1. + +Flag 1 is one of the four published flags whose target final contains the +basis head. Frames are binary subspaces of the nine-dimensional label space, +so hosting is checked both as literal frame membership and as membership in +the GF(2) span of the frame. Admission uses need() and remains active under +python -O. This module does not import independent.py or any predecessor +verifier. +""" + +import hashlib +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +MARKER = ( + "PASS_P104_PRESENT_HEAD_FLAG1 flag=1 head=232 preterminal_hosting=0 " + "preterminal_span_hosting=0 drop_event=591 arrive_event=3473 " + "source_span_drops=0 head_free_target_updates=6/6 no_new_kappa" +) +INPUTS = ( + "research/p104-joint-unit-flags/CERTIFICATE.json", + "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "research/p104-endpoint-geometric-budget/geometry.py", +) +SOURCE_LINE = "sources = [paths[f'X{s}'] for s in range(104)]" +TARGET_LINE = "targets = [paths[f'Y{t}'] for t in range(104)]" +FLAG_INDEX = 1 +HIT_FLAGS = (0, 1, 9, 43) +LABEL_BITS = 9 + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def pairs_unique(pairs): + value = {} + for key, item in pairs: + need(key not in value, "duplicate JSON key") + value[key] = item + return value + + +def read_json(path): + raw = Path(path).read_bytes() + need(len(raw) <= 2_000_000, "input exceeds 2 MB") + return json.loads(raw, object_pairs_hook=pairs_unique) + + +def register_name(item): + if type(item) is not str or len(item) < 2 or item[0] not in "XY": + return None + if not item[1:].isdigit() or int(item[1:]) > 103: + return None + return item + + +def annotated_frames(event, name): + frames = [] + if event[0] == "transport" and event[1] == name: + need(type(event[2]) is list and type(event[3]) is list, "transport frames") + frames.append(("before", list(event[2]))) + frames.append(("after", list(event[3]))) + elif event[0] == "add" and name in (event[1], event[2]): + need(type(event[-1]) is list, "add frame") + frames.append(("add", list(event[-1]))) + return frames + + +def echelon(frame): + """Pivot-indexed GF(2) row echelon form; each row tracks its frame subset.""" + rows = {} + for vector in frame: + need(type(vector) is int and 0 < vector < (1 << LABEL_BITS), "label range") + value = vector + combo = 1 << frame.index(vector) + while value: + pivot = value.bit_length() - 1 + if pivot not in rows: + rows[pivot] = (value, combo) + break + value ^= rows[pivot][0] + combo ^= rows[pivot][1] + need(value != 0, "dependent frame vector") + return rows + + +def span_combination(vector, frame): + """Return the frame subset whose XOR is vector, or None if outside the span.""" + rows = echelon(frame) + value = vector + combo = 0 + while value: + pivot = value.bit_length() - 1 + if pivot not in rows: + return None + value ^= rows[pivot][0] + combo ^= rows[pivot][1] + return sorted(frame[i] for i in range(len(frame)) if combo >> i & 1) + + +def in_span(vector, frame): + return span_combination(vector, frame) is not None + + +def rank(frame): + return len(echelon(frame)) + + +def span_elements(frame): + rows = [row for row, _ in echelon(frame).values()] + out = [] + for mask in range(1 << len(rows)): + value = 0 + for i, row in enumerate(rows): + if mask >> i & 1: + value ^= row + out.append(value) + return sorted(out) + + +def span_contains(big, small): + return all(in_span(vector, big) for vector in small) + + +def pin_sources(root=ROOT, here=HERE): + manifest = read_json(here / "SOURCES.json") + rows = manifest["files"] + inputs = [row for row in rows if row["usage"] == "input"] + need(tuple(row["path"] for row in inputs) == INPUTS, "input inventory") + pinned = {} + for row in inputs: + path = root / row["path"] + raw = path.read_bytes() + need(len(raw) <= 2_000_000, "source size") + digest = hashlib.sha256(raw).hexdigest() + need(digest == row["sha256"], "source hash: " + row["path"]) + pinned[row["path"]] = raw + return pinned + + +def hit_flag_indices(helpers, witness): + hits = [] + for index, row in enumerate(helpers): + head = row["basis"][0] + target = f"Y{row['target']}" + if head in witness["final_frames"][target]: + hits.append(index) + return hits + + +def build_receipt(witness, helpers): + need(len(helpers) == 208, "flag count") + need(len(witness["program"]) == 4058, "word length") + hits = hit_flag_indices(helpers, witness) + need(hits == list(HIT_FLAGS), "hit-flag census drift") + need(FLAG_INDEX in hits, "flag 1 left the present-head class") + helper = helpers[FLAG_INDEX] + head = helper["basis"][0] + source = f"X{helper['source']}" + target = f"Y{helper['target']}" + program = witness["program"] + source_events = [] + target_events = [] + joint = 0 + source_head = [] + target_head = [] + target_vectors = set() + source_frames = 0 + source_span_frames = 0 + source_span_drops = [] + target_span_head = [] + target_updates = [] + target_updates_head_free = [] + transports = [] + for index, event in enumerate(program): + need(type(event) is list and 1 <= len(event) <= 8, "event shape") + names = [] + for item in event: + name = register_name(item) + if name is not None: + names.append(name) + if source in names and target in names: + joint += 1 + if source in names: + source_events.append(index) + for role, frame in annotated_frames(event, source): + source_frames += 1 + if in_span(head, frame): + source_span_frames += 1 + else: + source_span_drops.append(index) + if head in frame: + source_head.append( + { + "event": index, + "opcode": event[0], + "role": role, + "frame": sorted(frame), + } + ) + if event[0] == "transport" and event[1] == source: + transports.append(event) + if target in names: + target_events.append(index) + for role, frame in annotated_frames(event, target): + target_vectors.update(frame) + if in_span(head, frame): + target_span_head.append({"event": index, "role": role}) + if head in frame: + target_head.append( + { + "event": index, + "opcode": event[0], + "role": role, + "frame": sorted(frame), + } + ) + if event[0] == "add" and event[1] == target: + target_updates.append(index) + if not in_span(head, event[-1]): + target_updates_head_free.append(index) + if event[0] == "transport" and event[1] == target: + transports.append(event) + need(source_events and target_events, "endpoint silence") + drop = source_events[0] + drop_event = program[drop] + need(drop_event[0] == "transport" and drop_event[1] == source, "first source op") + need(drop_event[2] == [head], "drop before-frame") + need(head not in drop_event[3], "drop after-frame still lists head") + after_drop = False + for row in source_head: + if row["event"] > drop: + after_drop = True + if row["event"] == drop and row["role"] == "after": + after_drop = True + need(len(target_head) == 1, "unexpected target head hosting count") + arrive = target_head[0] + need(arrive["opcode"] == "transport", "arrive opcode") + need(arrive["role"] == "after", "arrive role") + need(arrive["event"] == target_events[-1], "arrive is not terminal target event") + preterminal = [row for row in target_head if row["event"] < arrive["event"]] + need(preterminal == [], "preterminal target hosting") + arrive_event = program[arrive["event"]] + need(arrive_event[0] == "transport" and arrive_event[1] == target, "arrive transport") + need(head not in arrive_event[2], "arrive before-frame already lists head") + need(head in arrive_event[3], "arrive after-frame missing head") + hosting_gap = arrive["event"] - drop + need(hosting_gap > 0, "arrive precedes drop") + need(target_span_head, "target never span-hosts head") + span_arrive = target_span_head[0] + span_preterminal = [ + row for row in target_span_head if row["event"] < arrive["event"] + ] + nested = all(span_contains(event[3], event[2]) for event in transports) + rank_steps = all( + event[4] == rank(event[3]) - rank(event[2]) for event in transports + ) + decomposition = span_combination(head, list(drop_event[3])) + finals_with_head = sum( + 1 for index in range(104) if head in witness["final_frames"][f"Y{index}"] + ) + source_initial = witness["initial_frames"][source] + source_final = witness["final_frames"][source] + target_initial = witness["initial_frames"][target] + target_final = witness["final_frames"][target] + cohost_open = span_arrive["event"] + return { + "schema_version": 1, + "claim_id": "p104-present-head-flag1-audit", + "pinned_main": "6f100d4bb5083f8c35d96fd95a539811c62f245c", + "flag_index": FLAG_INDEX, + "source": helper["source"], + "target": helper["target"], + "basis_head": head, + "departure_choice": helper["departure_choice"], + "arrival_choice": helper["arrival_choice"], + "basis": helper["basis"], + "source_register": source, + "target_register": target, + "source_initial": source_initial, + "source_final": source_final, + "target_initial": target_initial, + "target_final": target_final, + "source_initial_is_basis_head": source_initial == [head], + "target_final_contains_basis_head": head in target_final, + "source_frame_restored": sorted(source_initial) == sorted(source_final), + "target_frame_restored": sorted(target_initial) == sorted(target_final), + "source_rank_initial": rank(source_initial), + "source_rank_final": rank(source_final), + "target_rank_initial": rank(target_initial), + "target_rank_final": rank(target_final), + "source_first_event": source_events[0], + "source_last_event": source_events[-1], + "target_first_event": target_events[0], + "target_last_event": target_events[-1], + "source_event_count": len(source_events), + "target_event_count": len(target_events), + "joint_source_target_events": joint, + "basis_head_drop_event": drop, + "basis_head_drop_before": sorted(drop_event[2]), + "basis_head_drop_after": sorted(drop_event[3]), + "basis_head_arrive_event": arrive["event"], + "basis_head_arrive_before": sorted(arrive_event[2]), + "basis_head_arrive_after": sorted(arrive_event[3]), + "hosting_gap_events": hosting_gap, + "source_annotations_containing_basis_head": len(source_head), + "target_annotations_containing_basis_head": len(target_head), + "target_preterminal_annotations_containing_basis_head": len(preterminal), + "source_head_annotations": source_head, + "target_head_annotations": target_head, + "target_annotated_vectors": sorted(target_vectors), + "basis_head_in_any_target_annotation": head in target_vectors, + "basis_head_in_source_after_drop": after_drop, + "drop_after_span_decomposition_of_head": decomposition, + "drop_transport_span_nested": span_contains(drop_event[3], drop_event[2]), + "source_annotation_count": source_frames, + "source_annotations_span_hosting_basis_head": source_span_frames, + "source_span_drop_events": source_span_drops, + "target_span_first_hosting_event": span_arrive["event"], + "target_span_first_hosting_role": span_arrive["role"], + "target_preterminal_annotations_span_hosting_basis_head": len(span_preterminal), + "target_arrive_before_span": span_elements(list(arrive_event[2])), + "target_update_events": target_updates, + "target_updates_in_head_free_span": len(target_updates_head_free), + "target_last_update_event": target_updates[-1], + "target_events_after_span_cohost_open": sum( + 1 for index in target_events if index > cohost_open + ), + "source_events_after_span_cohost_open": [ + index for index in source_events if index > cohost_open + ], + "endpoint_transport_count": len(transports), + "endpoint_transports_span_nested_upward": nested, + "endpoint_transport_rank_steps_match": rank_steps, + "targets_whose_final_contains_basis_head_among_all": finals_with_head, + "hit_flags_from_census": list(HIT_FLAGS), + "flag_is_present_head_case": True, + "obstruction": ( + "published_channel_hosts_basis_head_on_matched_target_only_at_" + "terminal_transport_literally_and_in_span_after_every_target_update" + ), + "no_new_kappa": True, + "selected_kappa": "0.001672660197076918", + } + + +def evaluate(root=ROOT, here=HERE): + pinned = pin_sources(root, here) + geometry = pinned[ + "research/p104-endpoint-geometric-budget/geometry.py" + ].decode("utf-8") + need(SOURCE_LINE in geometry, "source naming left the geometry") + need(TARGET_LINE in geometry, "target naming left the geometry") + certificate = json.loads( + pinned["research/p104-joint-unit-flags/CERTIFICATE.json"], + object_pairs_hook=pairs_unique, + ) + witness = json.loads( + pinned["research/p104-native-channel/inputs/LOWRANK-WITNESS.json"], + object_pairs_hook=pairs_unique, + ) + receipt = build_receipt(witness, certificate["helpers"]) + need(receipt["target_final_contains_basis_head"] is True, "left present-head class") + need(receipt["target_preterminal_annotations_containing_basis_head"] == 0, "preterminal") + need(receipt["target_annotations_containing_basis_head"] == 1, "target hosting count") + need(receipt["basis_head_drop_event"] == 591, "drop event drift") + need(receipt["basis_head_arrive_event"] == 3473, "arrive event drift") + need(receipt["hosting_gap_events"] == 2882, "gap drift") + need(receipt["basis_head_in_source_after_drop"] is False, "source relisted head") + need(receipt["joint_source_target_events"] == 0, "joint endpoint event") + need(receipt["source_frame_restored"] is False, "source restored") + need(receipt["target_frame_restored"] is False, "target restored") + need(receipt["source_span_drop_events"] == [], "source lost head direction") + need( + receipt["source_annotations_span_hosting_basis_head"] + == receipt["source_annotation_count"], + "source span hosting gap", + ) + need(receipt["target_span_first_hosting_event"] == 3473, "span arrive drift") + need(receipt["target_span_first_hosting_role"] == "after", "span arrive role") + need( + receipt["target_preterminal_annotations_span_hosting_basis_head"] == 0, + "preterminal span hosting", + ) + need( + receipt["target_updates_in_head_free_span"] + == len(receipt["target_update_events"]) + == 6, + "target update in head-hosting chart", + ) + need(receipt["target_events_after_span_cohost_open"] == 0, "target event after cohost") + need(receipt["endpoint_transports_span_nested_upward"] is True, "non-nested transport") + need(receipt["endpoint_transport_rank_steps_match"] is True, "rank step mismatch") + need(receipt["no_new_kappa"] is True, "kappa claim crept in") + return receipt + + +def admit(observed, expected): + need(observed == expected, "certificate mismatch") + + +def main(): + observed = evaluate() + expected = read_json(HERE / "CERTIFICATE.json") + admit(observed, expected) + print(MARKER) + + +if __name__ == "__main__": + main()