Archive C verification batching and failed complete speed gates

research/c-verification-feasibility/CODE-SOURCES.json

@@ -0,0 +1,21 @@
+{
+  "drivers/baseline_full.py": "470096a40078958bd4e32f99e312a44672613c2d93a76c9cbfd8d8fb6474471f",
+  "drivers/candidate_full.py": "e0978a90c63e5294a1ed04863c3966016b64a62a561e914d50821b08846ace72",
+  "full_B.py": "805d68c55f6565da489a90504e5488ce1636ebdb7be0c7b7e730227a5dad54de",
+  "full_C.py": "2800f8785d719152a99c70a561ce54ab7b1a5f6482fb40d50766aa93beafcf5d",
+  "guard.py": "7540f8cc4ae4d12ed86c844ef0837a74184d3ada653979608c295c09f200a751",
+  "integer/finite_probe.py": "1b804c882833e2628d843bade00dfcbb282e0f53f6712e2d978af9b5c1ce8378",
+  "integer/integer_binding.py": "dd3e4387dfb8882a524d938d866ed7ae04cd5ac938bbbcbec4eefd15f4bdcc9d",
+  "integer/integer_format.c": "804cc25bd9ad0912de81fe97bc65b95ebcb0dec06453739e1d4863e7946c4f3d",
+  "integer/micro_probe.py": "f1d39f830987fcabe8ca5453ddbb1eca1df10a9670a95db510efbe5f21dd76aa",
+  "integer/native_loader.py": "2592bef50e5338ad562d9a69bca1183ef0d88a4d34bdc497af4452304dca25c3",
+  "owned_integer/diagnostic.py": "4efeb040398c6d5204d552b6211e5a99aa3a3cb156ca422f05fbf0edd58e817b",
+  "owned_screen.py": "93fe1f8039e3a3442f561eb5463182d558d459d7335c882b009256780539419e",
+  "portable.py": "77f8910fb9ba1ed8dcc23bc574e2998105b86818f7391b48efa77eda6ea3d859",
+  "rational/arithmetic_binding.py": "db9c2778be538e1a7ae975b7e2108e52da53600a268c76d5e27b9965f0bb622a",
+  "rational/bulk_backend.py": "9b440bd3d921bb06ff5035cb8ae85053f3e0b6880b6ec37d364b55da012449ca",
+  "rational/finite_probe.py": "362bcd2bc967ed223ed303835048d1c51697f0293cfc83cffd4a9e02e2efcccd",
+  "rational/native_bulk.c": "4a4949e36cff4ff2894dd1f9379b58a58346ec7c888903271d4b98bbe4cfc7ae",
+  "replay.py": "ec80c3da976fe23987ce7da568185ee0d76a28f7c6ac38c8a5cf969c3cf6603c",
+  "verify.py": "6c25ffb97cbe940f8414d97c668a0b0d2d759e0d37d46283316e577b7bb38372"
+}

research/c-verification-feasibility/README.md

@@ -0,0 +1,205 @@
+# C verification feasibility: rational batching, integer loops and witness bytes
+
+This source-pinned engineering screen retains useful exact C prototypes and a
+negative complete-performance result. **It does not establish a further 15%
+improvement or any qualified positive increment over PR5864.** All six retained
+frozen-qualifier scientific receipts agree, but the integer/format candidate
+fails both the 15% target and the declared conservative noise gate. The rational
+candidate stops at an adverse independent-oracle cost screen.
+
+This evaluates priorities 1, 2 and 4 of the donor's four-opportunity review.
+Exact matrix/GF(2) kernels are a separate workload and are not credited toward
+the PR5864 target. No kappa, mathematical construction, physical-cost,
+selected-frontier, merge or maintainer-acceptance claim is made.
+
+## Fixed question and sources
+
+Can further C exact-arithmetic or serialization work accelerate the complete
+frozen PR5864 qualifier while preserving its inputs, independent numerical
+contracts, output types, full signed witnesses, hashes and coverage?
+
+Canonical main is `de5ec2e7a6074068452f45b1a191b5c72832df4a`. The official
+163-file PR5864 export is pinned at
+`3f15c943e4ad6479f03e674c80fff1269a16ccfe`, SHA-256
+`7b142567acacac5182045bf8daa8780e916661c2cf343dbf81b13c88ead85d64`.
+The immutable input retains the complete attribution and predecessor chain.
+The original archives, packages and mathematical sources are unchanged.
+
+Nearest predecessors are [PR5848](https://github.com/CrocSwap/integer-mult-bounds/pull/5848),
+[PR5852](https://github.com/CrocSwap/integer-mult-bounds/pull/5852),
+[PR5853](https://github.com/CrocSwap/integer-mult-bounds/pull/5853),
+[PR5864](https://github.com/CrocSwap/integer-mult-bounds/pull/5864) and the scoped
+negative score-dispatch [PR5875](https://github.com/CrocSwap/integer-mult-bounds/pull/5875).
+The visible open Fraction PR search and active discussion search are bounded
+overlap checks, not exhaustive novelty evidence.
+
+## Integer loops and canonical formatting: exact outputs, failed performance gate
+
+The candidate changes the integer `Engine` implementation: checked C batches
+sparse additions, signed score updates, scaling, reverse updates and canonical
+dyadic byte formatting using arbitrary-size Python integers. The PR5864
+Fraction numerical operations, contribution cache and native bookkeeping remain
+unchanged. They provide the same separately executed comparison path, with
+shared CPython big-integer primitives acknowledged. This does not claim wholly
+independent arithmetic implementations.
+
+All original timed finite/native/Observation checks and the 120 independent
+fixtures remain active. All actual ideal metadata, local weights, error traces,
+signed witness rows, reverse comparisons, hashes and the frozen scientific
+receipt remain equal on 25,984 events and 799 coordinates. Added finite checks
+cover eight row cases, six ordered prefixes, 8,192-bit values, signed
+cancellation, complete byte ordering, aliases and 27 labeled checks (six positive
+groups and 21 rejection paths). Normal and optimized finite modes pass.
+
+Each candidate timing pays the added C compile/link/load and every added finite
+check. GNU time includes compiler-child CPU. The fixed order is B,C,C,B,B,C;
+every sample is retained in [the raw runs](evidence/runs/).
+
+| Complete frozen qualifier | Median wall seconds | Median CPU seconds |
+| --- | ---: | ---: |
+| PR5864 baseline | 34.661785392 | 34.47 |
+| Integer/format candidate | 32.418777812 | 32.33 |
+| Observed fractional reduction | 6.4711% | 6.2083% |
+| Maximum within-arm repeat spread | 2.713637238 | 2.35 |
+| Absolute median saving | 2.243007580 | 2.14 |
+
+The observed median savings are smaller than their repeat spreads. The
+predeclared final gate requires an absolute saving greater than 0.50 seconds
+and either arm's observed spread in both wall and CPU, plus the 15% target.
+Both noise gates and the target fail. These observations are not a qualified
+speedup. No sample was discarded and no timing was rerolled. See
+[INTEGER-COMPLETE-GATE.json](evidence/INTEGER-COMPLETE-GATE.json).
+
+The timed scope matches PR5864's `benchmark.py` / `full_C.py` frozen qualifier.
+As in that predecessor, four unchanged source-custody controls are separate
+from both timed arms. The registered baseline command below freshly runs them
+with all predecessor finite/native checks. The timings are not the larger
+portable `replay_driver.py` total. A new full optimized or readonly complete
+performance qualification was not pursued after the failed gate.
+
+The internal `add_row` helper now returns a fresh dictionary. The compatibility
+promise is the checked `Engine` workload contract; arbitrary external callers
+expecting mutation/`None` are not covered. Historical binder metadata fields
+such as `source_only_handoff` describe the worker's handoff, while the parent
+run receipts state what was actually executed.
+
+## Broader integer ownership: one rejection-only cost diagnostic
+
+Before constructing another integer state owner, one source-bound diagnostic
+ran the original PR5864 qualifier without replacing arithmetic. A facade timed
+4 original ideal, 121 error-trace and 121 reverse calls, accounting for their
+disjoint union and retaining every scientific check and exception. No timing
+sample was rerolled or added to the BCCBBC comparison.
+
+The observed eligible union was 4.855752 wall / 4.853204 CPU seconds, below the
+fixed 15% thresholds of 5.199268 / 5.170500 seconds from the chosen baseline
+medians, even granting zero replacement and validation costs. The diagnostic's
+whole command was faster than those earlier baseline samples; these are scoped
+observations under host variation, not a machine-independent upper bound or
+universal obstruction. Relative to its own entire command the free union is
+only about 15.2%, before retained computation and added controls. No fully
+priced construction is funded by this screen.
+
+[All 246 boundary records](evidence/INTEGER-OWNED-BOUNDARY-SCREEN.json), the
+unchanged [diagnostic source](owned_integer/diagnostic.py), and the
+[complete ownership-cost review](evidence/astra-next-boundary-cost-screen.md)
+remain visible. Optional guarded arm `D` reproduces this diagnostic; it is not
+a performance sample or permission to repeat a failed screen automatically.
+
+## Rational batching: independent-oracle bill stops construction
+
+The prototype retains the existing contribution callback/cache and batches
+three score accumulators as general normalized rational pairs backed by Python
+integers. It materializes exact built-in Fractions at each event boundary and
+supports odd denominators. Exact Fraction output types do not make its changed
+arithmetic an untouched literal Python Fraction oracle.
+
+The bounded probe passed 178 literal/predecessor/candidate comparisons and 19
+added controls. The final binder also rejects destructor and unknown-source drift; its exact final
+bytes pass finite normal and optimized replay. The earlier binder and every
+declared BCCB micro observation are retained. The micro excludes cold build
+and has no complete-performance or source-independent oracle admission.
+
+Under the required literal-oracle contract, a complete candidate must pay for
+the untouched literal Fraction path, the unchanged integer path, and the new
+rational path with separate mutable state. Historical, same-audit observations
+retained inside the official export give 20.534678 wall / 20.523067 CPU seconds
+for the literal trace and 11.886980 wall / 11.883083 CPU seconds for the entire
+replaceable native trace including cold build. Even granting zero cost to the
+new rational kernel, conversions, build and all new checks, that replacement
+adds about 8.65 wall / 8.64 CPU seconds in this historical screen.
+
+This defeats credible headroom for this exact restoration design. It is a
+source-pinned engineering stop, not a fresh complete benchmark, universal
+runtime lower bound, or impossibility result. No new actual-word or complete
+rational run was performed. The source-qualified packet interface does not
+promise arbitrary callback observational equivalence or allocator-level OOM
+partial-state equivalence. See [the detailed report](evidence/astra-rational-design.md)
+for the complete added validation bill and unresolved construction obligations.
+
+## Fresh verification and reproduction
+
+Tested on Linux x86-64, CPython 3.12.3 and GCC 13.3. Existing `cc` and Python
+development headers are required. No dependency installation, compiled binary,
+new mathematical search or shared mutable answer cache is included.
+
+```sh
+python3.12 -B scripts/research_package.py --package research/c-verification-feasibility
+```
+
+The registered commands freshly authenticate the full export and exact prototype
+code, run the original custody/finite/native verifier, and run integer and
+rational finite checks in normal and optimized modes. They do not execute the
+actual word or admit performance. Source export and readonly Git-free finite
+verification are independent packaging checks.
+
+For a separately authorized complete correctness replay, the guarded optional
+entry point takes a new external evidence directory and an arm:
+
+```sh
+python3.12 -B research/c-verification-feasibility/replay.py C /tmp/c-feasibility-new-evidence
+```
+
+This reconstructs the exact scientific source layout from the archive and adds
+portable extraction overhead. Its fresh times are separate from the retained
+six-process screen. It refuses evidence reuse and retains the 180-second /
+1-GiB sampled process-group RSS / serial / zero-automatic-retry policy. Do not
+reroll the failed retained timing round.
+
+## Hosted runtime correction
+
+The first hosted replay rejected CPython 3.12.15 at the strict full-file
+Fraction source hash, after the baseline and integer normal/optimized checks
+passed. The failure is retained. An explicit second reviewed source hash admits
+the official 3.12.15 file; its only source difference is in `Fraction.__pow__`,
+outside the bypassed score operations. Exact live operation, closure, defaults,
+MRO and descriptor checks remain. Unknown source bytes reject even after the
+expected-code cache is populated. This compatibility correction changes no
+measured integer source, C kernel, timing sample or failed performance gate.
+See [the retained correction](evidence/publication/CI-PORTABILITY-CORRECTION.json).
+
+## Credit
+
+Original mathematics, P104 source, integer replay, literal scalar and reverse
+oracles: Ali Romman and all predecessor authors retained in the complete input
+archive and its NOTICE. Earlier source-bound contribution-table, entry,
+compact/slot and C-bookkeeping work is retained and credited through PR5852,
+PR5853 and PR5864; PR5875 supplies the separate failed thin score-dispatch
+screen. The inherited Ali Romman PR5761 three-file routing-test repair remains
+credited and unchanged. Apache-2.0 notices remain in the archive and new source.
+
+Prepared by Chris R / Clear1nsight with substantial OpenAI Codex implementation
+and user-requested GPT-6-astra xhigh static design/source review. Only the parent
+ran numerical/compiler work, serially. These are assisted engineering checks,
+without independent human or proof-kernel acceptance.
+
+## Open next questions
+
+The requested further 15% PR5864 improvement remains unmet. A different exact
+arithmetic ownership boundary would need a new source-pinned cost screen,
+unchanged required independent oracle and full added verification bill before
+construction. No further timing or construction is justified for these frozen
+nominations in this round. The separate matrix/GF(2) opportunity must be priced
+against its own complete verification scope; its savings cannot be added to
+these percentages. [Structured questions](TASK.json) and both retained design
+reports name the boundaries and smallest useful next steps.

research/c-verification-feasibility/SOURCES.json

@@ -0,0 +1,51 @@
+{
+  "schema_version": 1,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "files": [
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "research/c-verification-feasibility/inputs/PR5864.tar",
+      "usage": "input",
+      "git_blob": "bb9fc302168df0bf66cf43d08bce70544eeffc4e",
+      "sha256": "7b142567acacac5182045bf8daa8780e916661c2cf343dbf81b13c88ead85d64",
+      "pin": "head:ccb92b752ab31df4220780a580cc14d9e86ffeca:research/c-verification-feasibility/inputs/PR5864.tar"
+    }
+  ],
+  "external_origin": {
+    "repository": "CrocSwap/integer-mult-bounds",
+    "pr": 5864,
+    "head": "3f15c943e4ad6479f03e674c80fff1269a16ccfe",
+    "official_export_sha256": "7b142567acacac5182045bf8daa8780e916661c2cf343dbf81b13c88ead85d64",
+    "complete_files": 163
+  },
+  "predecessors": [
+    5848,
+    5852,
+    5853,
+    5864,
+    5875
+  ],
+  "scope": "No new kappa, construction, selected-frontier or qualified performance claim.",
+  "runtime_fraction_source_pins": [
+    {
+      "sha256": "cf33568f7b767f66896995a7a81cc662e8be226f2e58efb61d2028f64eb5d231",
+      "origin": "local Linux CPython3.12.3 stdlib, unchanged timed environment"
+    },
+    {
+      "sha256": "d52d1ab9d5be26924e4914a5e40069c992bbfa68f773694c2e5ee8452d0766a0",
+      "origin": "https://raw.githubusercontent.com/python/cpython/v3.12.15/Lib/fractions.py",
+      "scope": "explicit compatibility pin; all live operation shape guards retained"
+    }
+  ]
+}

research/c-verification-feasibility/TASK.json

@@ -0,0 +1,60 @@
+{
+  "schema_version": 1,
+  "task_id": "replay-runtime",
+  "original_card": {
+    "id": "replay-runtime",
+    "question": "Can one measured replay bottleneck be sped up without dropping coverage?",
+    "starting_points": [
+      "scripts/run_isolated_tests.py",
+      "scripts/verify_replay_coverage.py",
+      "certificates/selected-result.json"
+    ],
+    "methods": [
+      "Profile one isolated replay and optimize the measured bottleneck.",
+      "Design source-bound reuse with explicit dependency invalidation and negative controls."
+    ],
+    "acceptance_gate": "Report before/after wall time on the same fixture, retained checks and invalidation behavior.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "Measure one unchanged fixture, preserve check coverage, and test one optimization with invalidation controls.",
+    "bottleneck_link": "Faster trustworthy replays increase review throughput and let mechanism candidates be checked sooner.",
+    "allowed_variations": [
+      "Profile one stage or design one source-bound cache boundary."
+    ],
+    "scope_change_triggers": [
+      "Skipping coverage or comparing different fixtures to claim speedup."
+    ],
+    "overlap_terms": [
+      "replay runtime",
+      "cache invalidation",
+      "isolated tests"
+    ]
+  },
+  "bottleneck_link": "Faster trustworthy replays increase review throughput and let mechanism candidates be checked sooner.",
+  "author": "Chris R / Clear1nsight",
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "scope_status": "refined",
+  "scope_change_reason": "User requested all four C verification opportunities and a minimum15% improvement. This scoped package retains rational oracle-cost rejection and integer/format frozen-qualifier negative performance screen; matrix verification is separate.",
+  "actual_scope": "PR5864/source-pinned-C-rational-integer-format-feasibility",
+  "stop_rule": "No timing rerolls after failed noise/15% gates; no full rational run after adverse oracle-cost screen. Keep all scoped negative evidence and attribution.",
+  "time_budget_minutes": 60,
+  "outcome": "completed",
+  "evidence": "README.md, evidence/INTEGER-COMPLETE-GATE.json, evidence/runs/, exact source manifests and independent Astra source reviews",
+  "ai_assistance": "Substantial OpenAI Codex implementation and user-requested GPT-6-astra xhigh static source/design review. One parent-owned serial numerical runner; no human or proof-kernel acceptance.",
+  "open_questions": [
+    {
+      "question": "Could a different exact arithmetic ownership boundary fund a complete gain while retaining the required independent oracle?",
+      "why_it_matters": "The requested further15% frozen-qualifier target remains unmet by these mechanisms.",
+      "first_step": "Give a source-pinned static cost screen and complete validation bill before any new construction or timing round.",
+      "blocked_by": "Current rational oracle restoration is losing; integer/format samples failed the declared noise gate and15% target."
+    }
+  ]
+}