diff --git a/research/f7-sharp-cap-independent-audit/README.md b/research/f7-sharp-cap-independent-audit/README.md new file mode 100644 index 0000000000..1c1f0c9e97 --- /dev/null +++ b/research/f7-sharp-cap-independent-audit/README.md @@ -0,0 +1,187 @@ +# Independent audit of the sharp five-label cap + +**Corroboration; no new bound or kappa.** This answers Ali Romman's explicit +[independent-review handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19138920) +for [PR4992](https://github.com/CrocSwap/integer-mult-bounds/pull/4992). +The written-proof review below finds no blocking gap in its stated domain. +A separately implemented six-plus-six path join corroborates the cap **11** +and exclusion of every weight-four **(8,4)** split, without using either result +to discard a path. It imports no predecessor executable. + +The audited theorem concerns simple restored universal singleton-prefix walks +of length twelve in F2^5, and functionals of weight four or five. For the two +functional classes A,B, the excess is + +`choose(|A|,2) + choose(|B|,2) - |D(A)| - |D(B)|`, + +where D(C) contains XORs of distinct pairs in C. Shared differences in the two +classes count twice. Universality means the twelve vertices have all 32 XOR +sums, including zero. The result and both equality witnesses belong to the +predecessors; this package adds independent implementation and proof coverage. +This is AI-assisted review, not independent human or proof-kernel acceptance. + +## Written-proof audit + +Reviewed source: PR4992 head `12a0105150f5f44a19a2199db8506d1aa44b009a`, +retained at main base `f259dabc7d70e0db8d6d36bfda888f008bbfecc1`. +Its [proof](../f7-five-label-sharp-cap/README.md), verifier and receipt are +exactly bound in [SOURCES.json](SOURCES.json). They are authenticated, not +executed by the new verifier. The original registered verifier was also replayed +separately, in both normal and optimized Python. + +1. **Class coverage and balance.** Universality implies + `D(A) union D(B) = ker(f) minus {0}` because cross-class differences have + functional value one. For weight four, the omitted-coordinate edges form + a matching, including the closing edge. Counting degree two at every cycle + vertex gives `s-t=a-b`, `2a<=s`, `2b<=t`. Hence the only unordered splits + are (6,6), (7,5), (8,4). Weight five alternates and forces (6,6). +2. **Saturation in (8,4).** Equality forces four omitted-coordinate edges + in the majority, none in the minority, and eight crossing edges. Every + majority vertex belongs to exactly one matched pair. Contracting those + pairs leaves four distinct block labels T in the even subspace E of F2^4. + The four minority vertices alternate omitted-coordinate levels. No + planarity assumption on the minority is used. +3. **The potentially delicate repeated projection.** A planar T supplies only + seven lifted majority differences, insufficient even with six minority + differences. Thus T has six differences. Its missing direction z satisfies + `E = T disjoint-union (T+z)`. The minority must supply both missing lifts + (z,0) and (z,1). A same-level pair u,w=u+z occupies both vertices of one + level. A pair supplying (z,1) must use one of these vertices, so the other + level repeats u or w. Relabel to repeat u. The cyclic minority order is, + up to reversal and rotation, `u_0,u_1,w_0,y_1`; y=w is allowed. The four + distinct contracted blocks require at least three neighbors of u in T + and two of w. Translation by z exchanges T and its complement in E and + sends N(u) to N(w), so those two neighbor counts sum to four. This is + the claimed contradiction. Distinctness of the block labels, rather than + distinctness of all four projected minority points, justifies the count. +4. **Small support lemma.** Five, six or seven points have affine dimension + at least three. In dimension three their difference support is seven. + In dimension four an affine basis gives ten differences; a sixth point + of weight two or three gives twelve, and weight four gives fifteen. + To make the weight-three case explicit, translate + `{0,e1,e2,e3,e4,e1+e2+e3}` by e1 and use the basis + `(e1,e1+e2,e1+e3,e1+e4)`. The extra point is the sum of the second and + third basis vectors. Thus both twelve-support cases reduce to the source's + `{0,1,2,3,4,8}`. Its four-row table covers every possible seventh point + and contributes a new difference, giving at least thirteen. +5. **Final excess.** In (6,6), supports of size seven and seven cannot cover + fifteen directions, so their sum is at least 7+12. In (7,5), a + three-dimensional seven-point class would require the five-point class + to cover eight directions outside that subspace. Its two cosets supply + at most `k(5-k)<=6` such pairs. Hence the seven-point class has full + affine dimension; the support sum is at least 13+7. Both excess bounds + are eleven. The two cited words attain equality. + +This review covers the claimed proof implications, including the nonplanar +minority. It does not establish any seven-label or partial-prefix assertion. + +## Independent finite method and completeness + +The new enumerator lists **every simple six-edge cube path starting at zero**, +grouped by its final vertex. It joins every unordered pair with that same +endpoint whose vertex-set intersection is exactly the two endpoints. Reversing +one path yields a simple twelve-edge cycle, with the closing edge included. + +Conversely, split any simple twelve-edge cycle based at zero at its sixth +edge. Its two halves appear in these lists and have disjoint interiors. +The split is unique, and reversing the cycle only exchanges the halves. +Thus the join enumerates each cycle exactly once up to reversal. There is no +label-permutation reduction, universality prune, matching-balance prune, +quotient test, or excess prune in this generation step. + +After generation, direct pair XORs decide universality and compute each of +the six high-weight functionals. Every generated cycle separately passes +vertex, simplicity, adjacency and closing-edge checks. Six smaller domains +compare the complete cycle sets against literal enumeration of every word; +they also check that the join emits no duplicate cycle. + +| Quantity | Independently recomputed count | +|---|---:| +| All rooted cycles up to reversal in Q5, length 12 | 221,700 | +| Those using all five labels | 202,860 | +| Universal cycles | 49,680 | +| Universal cycle / high-weight functional checks | 298,080 | +| Universal weight-four (8,4) splits | 0 | +| Maximum excess for each of the six masks | 11 | +| Literal words in the six calibration domains | 77,019 | +| Distinct calibration cycles | 418 | + +The complete excess histogram agrees with PR4907's earlier receipt after +multiplying by 60. This comparison happens after generation and evaluation. +That factor is exact: a simple twelve-cycle uses four or five labels, and +both label orbit sizes in Q5 are 120; this audit then identifies the two +orientations. Summing over every high-weight functional preserves the same +factor. The prior 828 universal normalized words and their maxima are not +new discoveries. [RESULT.json](RESULT.json) retains the full histogram and +a digest of the deterministic universal-cycle stream. + +## Reproduction and controls + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/f7-sharp-cap-independent-audit +``` + +The registered commands run the independent audit normally and with `-O`, +then its mutation controls. Expect `PASS_F7_SHARP_CAP_INDEPENDENT_AUDIT`, +`PASS_F7_AUDIT_CONTROLS`, and `PASS_REGISTERED_RESEARCH_PACKAGE`. +One full enumeration took about five seconds locally on Windows 11 with +CPython 3.12.0; this is a reproduction estimate, not a speedup claim. +Direct commands, also valid in an export containing the declared inputs: + +```sh +python3.12 -I -B research/f7-sharp-cap-independent-audit/verify.py +python3.12 -I -O -W error -B research/f7-sharp-cap-independent-audit/verify.py +python3.12 -I -O -W error -B research/f7-sharp-cap-independent-audit/test_mutations.py +``` + +Eight semantic rejections cover the too-small cap, wrong functional domain, +length, repeated vertex, omitted closing edge, boolean vertex, nonuniversality +and a universal point set lacking the cycle contract. Both sharp witnesses +are positive controls. The set-only and low-weight counterexamples have +excess 18 and 21, respectively, and demonstrate why the hypotheses matter. + +Six actual code mutations exercise the small literal-word calibrations and +semantic controls **without receipt comparison**: overlapping path interiors, +a missing coordinate, a missing closing edge, coordinate-bit grouping, +cross-class support, and cap ten. Two additional private-copy CLI controls +alter the reviewed proof and replace integer 1 by boolean true in the receipt. +The latter requires typed JSON comparison. Frozen inputs are never edited. + +## Scope, coordination and credit + +Task `census-pruning-audit`, changed scope under the explicit handoff; priority +revision 7. [Canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/4903#discussioncomment-19140301). +The entry overlap check covered 324 open PRs and 4,127 Discussion records +with complete remote pagination. After materializing relevant f7 packages, +103 local records were searched; 6,609 tracked notes remained omitted. +Arbitrary diffs and unpublished work are also outside that coverage. +PR5001 and JoyboyBrian's active prefix-engine integration are separate. + +The source-binding orientation for selected #4470 passed. The selected kappa +remains `60403/20000000`. No selected cold replay, engine integration, +seven-label census, supplier admission, full multiplication theorem, Lean +or independent human review is claimed. Full-history ancestry preflight +is not claimed in this shallow checkout. The audit covers the exact pinned +proof and finite domain; later source changes require reassessment. + +Credit **Ali Romman / PR4992** for the sharp theorem and neighbor-count proof; +**Mihir Srivastava / PR4907** for the earlier cap, quotient setup, finite +measurements and handoff; **Nick Petalas / PR4894** for matching balance. +Retain **unpaidmoon / PR4148**, **Nicholas Stone / PR2973**, +**James Reed / PR3096**, and **Ross Richardson / PR943** for the question, +corrected excess boundary, audit and singleton-prefix model. The new algorithm +is separately implemented; the reviewer read the predecessor sources and +does not claim a blinded review. Original sources and notices are unchanged. +Prepared by Mihir Srivastava with substantial OpenAI Codex assistance, solo. +New work is Apache-2.0. + +## Open next questions + +Independent human or proof-assistant review can strengthen confidence in the +four-block contradiction; begin with step 3 above, including y=w, and the +explicit affine-basis change in step 4. This requires new review, not a larger +finite census. PR5001's partial-prefix contract and its already claimed engine +integration remain the relevant downstream work. This audit does not reserve +them or infer a runtime benefit. No larger census is justified by this result. diff --git a/research/f7-sharp-cap-independent-audit/RESULT.json b/research/f7-sharp-cap-independent-audit/RESULT.json new file mode 100644 index 0000000000..cb7a672a34 --- /dev/null +++ b/research/f7-sharp-cap-independent-audit/RESULT.json @@ -0,0 +1,186 @@ +{ + "audit": { + "all_cycles": 221700, + "all_five_labels": 202860, + "functional_checks": 298080, + "histogram": [ + { + "count": 25920, + "excess": 3, + "split": [ + 6, + 6 + ], + "weight": 4 + }, + { + "count": 83520, + "excess": 6, + "split": [ + 6, + 6 + ], + "weight": 4 + }, + { + "count": 5760, + "excess": 8, + "split": [ + 6, + 6 + ], + "weight": 4 + }, + { + "count": 7920, + "excess": 11, + "split": [ + 6, + 6 + ], + "weight": 4 + }, + { + "count": 31680, + "excess": 6, + "split": [ + 7, + 5 + ], + "weight": 4 + }, + { + "count": 48960, + "excess": 8, + "split": [ + 7, + 5 + ], + "weight": 4 + }, + { + "count": 25920, + "excess": 9, + "split": [ + 7, + 5 + ], + "weight": 4 + }, + { + "count": 18720, + "excess": 11, + "split": [ + 7, + 5 + ], + "weight": 4 + }, + { + "count": 11520, + "excess": 3, + "split": [ + 6, + 6 + ], + "weight": 5 + }, + { + "count": 33120, + "excess": 6, + "split": [ + 6, + 6 + ], + "weight": 5 + }, + { + "count": 2880, + "excess": 8, + "split": [ + 6, + 6 + ], + "weight": 5 + }, + { + "count": 2160, + "excess": 11, + "split": [ + 6, + 6 + ], + "weight": 5 + } + ], + "maxima_by_mask": { + "15": 11, + "23": 11, + "27": 11, + "29": 11, + "30": 11, + "31": 11 + }, + "universal_cycle_stream_sha256": "5caaa895d18de8f878566eb553d83cd4263b558bc0b34815184292470ad553d7", + "universal_cycles": 49680 + }, + "calibration": [ + { + "cycles": 1, + "length": 4, + "literal_words": 16, + "n": 2 + }, + { + "cycles": 3, + "length": 4, + "literal_words": 81, + "n": 3 + }, + { + "cycles": 12, + "length": 6, + "literal_words": 729, + "n": 3 + }, + { + "cycles": 6, + "length": 8, + "literal_words": 6561, + "n": 3 + }, + { + "cycles": 48, + "length": 6, + "literal_words": 4096, + "n": 4 + }, + { + "cycles": 348, + "length": 8, + "literal_words": 65536, + "n": 4 + } + ], + "controls": { + "low_weight_excess": 21, + "semantic_rejections": 8, + "set_only_excess": 18, + "sharp_witnesses": 2 + }, + "package_sha256": { + "README.md": "5ae16b49f957ab009194bdb85af4bcf63b27b62149c15d0f5cf09a6a83e812a5", + "SOURCES.json": "352f93ec3b588b3eac2bb71a8b0a391bbdad4ebb8fdf630f72e1669c8ade303c", + "TASK.json": "bbb17fa71a29a4cd3c6e3ad874fa9403f7b49aef27a1f0eeeab36109e99cf503", + "VERIFY.json": "4d61d05693e88246eb9129f456c859ccbc38137033a55df00a10a9ce7442d348", + "test_mutations.py": "09cdf95ed0f30eabfcf7f8a7e0776a7e2f1f8c783b7cb49bf7a5b99dd300c18e", + "verify.py": "e8ba74747f14dcce1bd14c6676c1214d1b38f76cc44590fc5468a7743045028c" + }, + "schema": "f7-sharp-cap-independent-audit/v1", + "source_sha256": { + "research/f7-five-label-pruning-proof/RESULT.json": "5bd83ffe534373471731bc59c6795ee864192882b6bd31683ffb44a88c864755", + "research/f7-five-label-sharp-cap/README.md": "c03f524035f4abeb9103e7e43486ee75b83538e41abb50cd3beaecd01119f871", + "research/f7-five-label-sharp-cap/RESULT.json": "08251f786df0070dea092ae180fc3fa5efe7b386aed04fa86aff601343bfd718", + "research/f7-five-label-sharp-cap/verify.py": "035687ed280ac001fc29c24f36ee7974966011206e11140891f9312ccefd69fb" + } +} diff --git a/research/f7-sharp-cap-independent-audit/SOURCES.json b/research/f7-sharp-cap-independent-audit/SOURCES.json new file mode 100644 index 0000000000..0a0e3a53e3 --- /dev/null +++ b/research/f7-sharp-cap-independent-audit/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "f259dabc7d70e0db8d6d36bfda888f008bbfecc1", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/f7-five-label-pruning-proof/RESULT.json", + "usage": "input", + "git_blob": "998371ad6ef619666752ec57e83d3531530f37c9", + "sha256": "5bd83ffe534373471731bc59c6795ee864192882b6bd31683ffb44a88c864755" + }, + { + "path": "research/f7-five-label-sharp-cap/README.md", + "usage": "input", + "git_blob": "1b80ac21964baf508859127126baac595dc9cdba", + "sha256": "c03f524035f4abeb9103e7e43486ee75b83538e41abb50cd3beaecd01119f871" + }, + { + "path": "research/f7-five-label-sharp-cap/RESULT.json", + "usage": "input", + "git_blob": "3fd9c9609bf0aaaf4224f495e3b10bb776a96c7f", + "sha256": "08251f786df0070dea092ae180fc3fa5efe7b386aed04fa86aff601343bfd718" + }, + { + "path": "research/f7-five-label-sharp-cap/verify.py", + "usage": "input", + "git_blob": "d5491b092b556c8fb5741bc28f277a6947474722", + "sha256": "035687ed280ac001fc29c24f36ee7974966011206e11140891f9312ccefd69fb" + } + ] +} diff --git a/research/f7-sharp-cap-independent-audit/TASK.json b/research/f7-sharp-cap-independent-audit/TASK.json new file mode 100644 index 0000000000..d722bb4d59 --- /dev/null +++ b/research/f7-sharp-cap-independent-audit/TASK.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "task_id": "census-pruning-audit", + "priority_revision": 7, + "base_commit": "f259dabc7d70e0db8d6d36bfda888f008bbfecc1", + "original_card": { + "id": "census-pruning-audit", + "question": "Does the reported word-census parity-pruning error invalidate a specific exclusion we still rely on, and what bounded repair is justified?", + "starting_points": [ + "research/f7-weight-parity-census-correction/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct the tiny counterexample and trace one affected exclusion to its exact pruning code.", + "Compare corrected and unpruned enumeration on a small exhaustive domain, then audit the changed pruning implication." + ], + "acceptance_gate": "Pin the old and proposed corrected engines, distinguish a disproved pruning rule from a disproved final bound, and state exactly which downstream exclusions need revalidation. #2973 is an author-checked source archive; neither its new f(7) claim nor all old conclusions are automatically accepted or rejected.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2973 error description and MATH.md; manually reconstruct the prefix states of 01021323 before running any large census.", + "scope": "Source-binding orientation only; no full enumeration or mathematical validation." + }, + "first_experiment": "Reconstruct the eight prefix states of 01021323 and compare bit-0 versus Hamming-weight parity budgets independently. Trace the reported false prune to one pinned predecessor (#2542, #2634 or #2691), then test a small exhaustive domain. Stop after a source-impact handoff or corrected-prune proof; a full seven-label replay needs a separate resource budget and a named research decision it can change.", + "bottleneck_link": "An unsound exclusion can wrongly close a mechanism; correcting its dependency boundary is more useful than extending the same census.", + "allowed_variations": [ + "One predecessor pruning rule, one independently exhaustive small domain, or one downstream dependency audit." + ], + "scope_change_triggers": [ + "Launching a larger census before validating the prune and explaining which active decision it changes.", + "Treating a small-domain counterexample to the old rule as a counterexample to every reported seven-label bound." + ], + "overlap_terms": [ + "2973", + "2542", + "2634", + "2691", + "weight parity", + "bit-0", + "01021323", + "census pruning" + ] + }, + "scope_status": "changed", + "actual_scope": "Independent written-proof and six-plus-six path-join audit of PR4992's cap 11 for simple restored universal five-label length-twelve walks.", + "scope_change_reason": "Handoff-first: Ali Romman explicitly requests independent proof review of PR4992. The older parity defect is already covered. PR5001 and JoyboyBrian's active engine integration are separate.", + "bottleneck_link": "Independent validation of a pruning-model theorem before downstream use; a scoped side audit, not a supplier or exponent improvement.", + "budget_minutes": 60, + "stop_rule": "Stop at corroboration or a concrete counterexample/coverage gap for n=5, L=12, weights four and five. No engine integration, larger census or selected replay.", + "outcome": "completed", + "evidence": "Written proof audit and separately implemented six-plus-six join: 221700 cycles, 49680 universal cycles, 298080 high-weight checks, all maxima 11, no universal (8,4) split. Six literal-word calibration domains; eight semantic rejections; six code mutations and two private integrity faults. Commands and exact scope in README.md and VERIFY.json.", + "author": "Mihir Srivastava", + "ai_assistance": "Substantial OpenAI Codex assistance for analysis, implementation, verification and publication; solo, no subagents or independent human review.", + "open_questions": [ + { + "question": "Can an independent human or proof assistant confirm the four-block neighbor contradiction and affine support reduction?", + "why_it_matters": "This contribution gives AI-assisted proof review and finite corroboration, not human or formal acceptance.", + "first_step": "Check README proof-audit steps 3 and 4, including the y=w minority case and explicit basis change. Existing PR5001 engine integration is separately claimed.", + "blocked_by": "Requires a genuinely separate reviewer or formal proof; enlarging this finite census would not discharge that obligation." + } + ] +} diff --git a/research/f7-sharp-cap-independent-audit/VERIFY.json b/research/f7-sharp-cap-independent-audit/VERIFY.json new file mode 100644 index 0000000000..580e4d61e8 --- /dev/null +++ b/research/f7-sharp-cap-independent-audit/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/f7-five-label-pruning-proof/RESULT.json", + "research/f7-five-label-sharp-cap/README.md", + "research/f7-five-label-sharp-cap/RESULT.json", + "research/f7-five-label-sharp-cap/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Independent six-plus-six cycle enumeration, six literal-word calibrations, sharp witnesses, semantic controls, source and typed receipt binding." + }, + { + "argv": ["{python}", "-I", "-O", "-W", "error", "-B", "{package}/verify.py"], + "timeout_seconds": 60, + "checks": "The complete independent audit with Python assertions disabled." + }, + { + "argv": ["{python}", "-I", "-O", "-W", "error", "-B", "{package}/test_mutations.py"], + "timeout_seconds": 60, + "checks": "Six actual code mutations with receipt comparison bypassed, plus private reviewed-source and typed-receipt corruptions." + } + ] +} diff --git a/research/f7-sharp-cap-independent-audit/test_mutations.py b/research/f7-sharp-cap-independent-audit/test_mutations.py new file mode 100644 index 0000000000..fcace143dd --- /dev/null +++ b/research/f7-sharp-cap-independent-audit/test_mutations.py @@ -0,0 +1,92 @@ +#!/usr/bin/env python3 +"""Require semantic mutants and private source/receipt faults to fail. + +Mihir Srivastava with substantial OpenAI Codex assistance. Apache-2.0. +""" +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +SOURCE = (PACKAGE / "verify.py").read_text(encoding="utf-8") + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def semantic_mutations(): + cases = ( + ("overlapping interiors", "if left_used & right_used == shared:", + "if True:", "calibrate"), + ("missing coordinate", "for coordinate in range(n):", + "for coordinate in range(n - 1):", "calibrate"), + ("missing closing edge", "zip(points, points[1:] + points[:1])", + "zip(points, points[1:])", "controls"), + ("bit-0 grouping", "(x & mask).bit_count() % 2 == bit", + "(x & 1) == bit", "controls"), + ("cross-class support", "support_bits(group).bit_count()", + "support_bits(points).bit_count()", "controls"), + ("cap ten", "def check_target(points, mask, cap=11):", + "def check_target(points, mask, cap=10):", "controls"), + ) + for name, old, new, entry in cases: + require(SOURCE.count(old) == 1, "mutation site: " + name) + namespace = {"__file__": str(PACKAGE / "verify.py"), "__name__": "audit_mutant"} + exec(compile(SOURCE.replace(old, new), str(PACKAGE / "verify.py"), "exec"), namespace) + try: + namespace[entry]() + except ValueError as error: + print("REJECT_MUTANT", name, str(error)) + else: + raise ValueError("surviving mutant: " + name) + return len(cases) + + +def integrity_faults(): + with tempfile.TemporaryDirectory(prefix="f7-audit-controls-") as temp: + root = Path(temp) + package = root / "research" / PACKAGE.name + shutil.copytree(PACKAGE, package) + manifest = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8")) + for row in manifest["files"]: + if row["usage"] == "input": + target = root / row["path"] + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / row["path"], target) + + def reject_cli(reason): + result = subprocess.run( + [sys.executable, "-I", "-O", "-B", str(package / "verify.py")], + cwd=root, text=True, encoding="utf-8", capture_output=True, timeout=60) + require(result.returncode != 0 and reason in result.stderr, + "private fault was not rejected at expected gate: " + reason) + + proof = root / "research/f7-five-label-sharp-cap/README.md" + original = proof.read_bytes() + proof.write_bytes(original + b"\nchanged reviewed proof\n") + reject_cli("source drift: research/f7-five-label-sharp-cap/README.md") + proof.write_bytes(original) + receipt_path = package / "RESULT.json" + receipt = json.loads(receipt_path.read_text(encoding="utf-8")) + require(type(receipt["calibration"][0]["cycles"]) is int and + receipt["calibration"][0]["cycles"] == 1, "typed fault fixture") + receipt["calibration"][0]["cycles"] = True + receipt_path.write_text(json.dumps(receipt), encoding="utf-8") + reject_cli("receipt mismatch") + return 2 + + +def main(): + mutations = semantic_mutations() + faults = integrity_faults() + print(f"PASS_F7_AUDIT_CONTROLS semantic_mutants={mutations} private_faults={faults}") + + +if __name__ == "__main__": + main() diff --git a/research/f7-sharp-cap-independent-audit/verify.py b/research/f7-sharp-cap-independent-audit/verify.py new file mode 100644 index 0000000000..7b7de67af2 --- /dev/null +++ b/research/f7-sharp-cap-independent-audit/verify.py @@ -0,0 +1,238 @@ +#!/usr/bin/env python3 +"""Independent path-join audit of PR4992; no predecessor code imports. + +Mihir Srivastava with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +from collections import Counter, defaultdict +from hashlib import sha256 +from itertools import combinations, product +import json +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +MASKS = (15, 23, 27, 29, 30, 31) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def json_bytes(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode("utf-8") + + +def canonical(cycle): + """Root stays zero; identify just the two traversal directions.""" + return min(cycle, (0,) + cycle[:0:-1]) + + +def half_paths(n, length): + endpoints = defaultdict(list) + stack = [((0,), 1)] + while stack: + path, used = stack.pop() + if len(path) == length + 1: + endpoints[path[-1]].append((path, used)) + continue + for coordinate in range(n): + neighbor = path[-1] ^ (1 << coordinate) + if not used & (1 << neighbor): + stack.append((path + (neighbor,), used | (1 << neighbor))) + return endpoints + + +def joined_cycles(n, length): + require(n >= 2 and length % 2 == 0 and 4 <= length <= 2**n, "domain") + for endpoint, paths in sorted(half_paths(n, length // 2).items()): + shared = 1 | (1 << endpoint) + for (left, left_used), (right, right_used) in combinations(paths, 2): + if left_used & right_used == shared: + yield canonical(left + right[-2:0:-1]) + + +def literal_cycles(n, length): + """Small independent oracle: all n**length words, without prefix pruning.""" + cycles = set() + for word in product(range(n), repeat=length): + points, state = [], 0 + for coordinate in word: + points.append(state) + state ^= 1 << coordinate + if state == 0 and len(set(points)) == length: + cycles.add(canonical(tuple(points))) + return cycles + + +def validate_cycle(points, n=5, length=12): + require(len(points) == length and points[0] == 0, "length/root") + require(all(type(x) is int and 0 <= x < 2**n for x in points), "vertex") + require(len(set(points)) == length, "simplicity") + require(all((x ^ y).bit_count() == 1 + for x, y in zip(points, points[1:] + points[:1])), "edge/closure") + + +def support_bits(points): + support = 0 + for x, y in combinations(points, 2): + support |= 1 << (x ^ y) + return support + + +def split_excess(points, mask): + classes = (tuple(x for x in points if (x & mask).bit_count() % 2 == bit) + for bit in (0, 1)) + sizes, value = [], 0 + for group in classes: + sizes.append(len(group)) + value += len(group) * (len(group) - 1) // 2 - support_bits(group).bit_count() + return tuple(sorted(sizes, reverse=True)), value + + +def check_target(points, mask, cap=11): + validate_cycle(points) + require(support_bits(points) == (1 << 32) - 2, "universality") + require(type(mask) is int and mask in MASKS, "mask") + split, value = split_excess(points, mask) + require(split in ((6, 6), (7, 5)), "split") + require(value <= cap, "cap") + return value + + +def word_points(word): + state, result = 0, [] + for character in word: + result.append(state) + state ^= 1 << int(character) + require(state == 0, "word closure") + return tuple(result) + + +def expect_rejection(action, reason): + try: + action() + except ValueError as error: + require(str(error) == reason, "wrong rejection") + return + raise ValueError("missed rejection: " + reason) + + +def controls(): + w4 = word_points("012343234031") + w5 = word_points("012343103432") + require(check_target(w4, 23) == check_target(w5, 31) == 11, "sharp witnesses") + expect_rejection(lambda: check_target(w4, 23, 10), "cap") + expect_rejection(lambda: check_target(w4, 1), "mask") + expect_rejection(lambda: validate_cycle(w4[:-1]), "length/root") + expect_rejection(lambda: validate_cycle(w4[:-1] + (w4[1],)), "simplicity") + expect_rejection(lambda: validate_cycle(w4[:-1] + (14,)), "edge/closure") + expect_rejection(lambda: validate_cycle((False,) + w4[1:]), "vertex") + nonuniversal = word_points("010201030203") + validate_cycle(nonuniversal) + expect_rejection(lambda: check_target(nonuniversal, 23), "universality") + set_only = (0, 3, 5, 9, 16, 19, 21, 25, 1, 14, 17, 30) + require(support_bits(set_only) == (1 << 32) - 2, "universal set control") + require(split_excess(set_only, 15) == ((8, 4), 18), "set-only excess") + expect_rejection(lambda: check_target(set_only, 15), "edge/closure") + require(split_excess(w4, 1)[1] == 21, "low-weight boundary") + return {"semantic_rejections": 8, "sharp_witnesses": 2, + "set_only_excess": 18, "low_weight_excess": 21} + + +def calibrate(): + report = [] + for n, length in ((2, 4), (3, 4), (3, 6), (3, 8), (4, 6), (4, 8)): + joined = list(joined_cycles(n, length)) + literal = literal_cycles(n, length) + require(len(joined) == len(set(joined)), "duplicate joined cycle") + require(set(joined) == literal, "literal-word calibration") + for cycle in joined: + validate_cycle(cycle, n, length) + report.append({"n": n, "length": length, "cycles": len(joined), + "literal_words": n**length}) + return report + + +def full_audit(): + counts = Counter() + histogram = Counter() + maxima = {str(mask): -1 for mask in MASKS} + cycle_hash = sha256() + for cycle in joined_cycles(5, 12): + validate_cycle(cycle) + counts["all_cycles"] += 1 + labels = 0 + for x, y in zip(cycle, cycle[1:] + cycle[:1]): + labels |= x ^ y + if labels == 31: + counts["all_five_labels"] += 1 + if support_bits(cycle) != (1 << 32) - 2: + continue + counts["universal_cycles"] += 1 + cycle_hash.update(bytes(cycle)) + for mask in MASKS: + split, value = split_excess(cycle, mask) + require(split in ((6, 6), (7, 5)), "universal split") + require(value <= 11, "universal cap") + histogram[(mask.bit_count(), split, value)] += 1 + maxima[str(mask)] = max(maxima[str(mask)], value) + counts["functional_checks"] += 1 + return {**dict(counts), "maxima_by_mask": maxima, + "universal_cycle_stream_sha256": cycle_hash.hexdigest(), + "histogram": [{"weight": weight, "split": list(split), + "excess": excess, "count": count} + for (weight, split, excess), count in sorted(histogram.items())]} + + +def source_bindings(): + manifest = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8")) + verified = {} + for row in manifest["files"]: + if row["usage"] == "input": + actual = sha256((ROOT / row["path"]).read_bytes()).hexdigest() + require(actual == row["sha256"], "source drift: " + row["path"]) + verified[row["path"]] = actual + return verified + + +def compare_predecessor(actual): + # Comparison only, after the complete independent census; no search decisions. + old = json.loads((ROOT / "research/f7-five-label-pruning-proof/RESULT.json").read_text( + encoding="utf-8"))["walks"] + for new_key, old_key in (("all_cycles", "canonical_closed"), + ("all_five_labels", "all_five_labels"), + ("universal_cycles", "universal"), + ("functional_checks", "functional_checks")): + require(actual[new_key] == 60 * old[old_key], "predecessor count: " + new_key) + expected = [dict(row, count=60 * row["count"]) for row in old["histogram"]] + require(actual["histogram"] == expected, "predecessor histogram") + require(actual["maxima_by_mask"] == old["maxima_by_mask"], "predecessor maxima") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit-receipt", action="store_true") + args = parser.parse_args() + pins = source_bindings() + checks = controls() + calibration = calibrate() + audit = full_audit() + compare_predecessor(audit) + receipt = {"schema": "f7-sharp-cap-independent-audit/v1", "controls": checks, + "calibration": calibration, "audit": audit, "source_sha256": pins, + "package_sha256": {name: sha256((PACKAGE / name).read_bytes()).hexdigest() + for name in ("README.md", "verify.py", "test_mutations.py", + "SOURCES.json", "TASK.json", "VERIFY.json")}} + if args.emit_receipt: + print(json.dumps(receipt, indent=2, sort_keys=True)) + else: + expected = json.loads((PACKAGE / "RESULT.json").read_text(encoding="utf-8")) + require(json_bytes(receipt) == json_bytes(expected), "receipt mismatch") + print("PASS_F7_SHARP_CAP_INDEPENDENT_AUDIT " + f"cycles={audit['all_cycles']} universal={audit['universal_cycles']} cap=11") + + +if __name__ == "__main__": + main()