Record that the V02 public replay does not bind the 56 assumptions

research/v02-assumption-binding-gap/README.md

@@ -0,0 +1,156 @@
+# V02 assumption values are not bound by the public replay
+
+**No κ change.** The selected frontier stays
+`363005817/100000000000`. This package does not justify the 56 recorded
+frontend facts, and it does not prove that any recorded value is false.
+
+## Scope and evidence
+
+This is item 1 of the open-request list taken from
+[#1166](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19530668):
+the 56 `original_source_condition_assumptions` in the V02 export, against the
+two-role contract. The parent-origin handoff on the same thread is a different
+request and is not done here.
+
+Catalogue card `formal-interface-lemma` asked for one uncovered interface
+binding. The scope is **changed**: the live handoff is the #7136 export and the
+frozen `pyinit_failure` / `exec_failure` commands, not a Lean lemma and not one
+of the five selected-frontier assumptions. The connection to the bottleneck is
+indirect. These assumptions are a prerequisite named by the V02 archive; they
+are not a selected-invoice term. A side result is still the requested audit.
+
+Pinned public export: Clear1nsight commit
+`1998ae8ee6d46bafac647329e5b41a85941bb2e7`, the commit named in that handoff.
+That commit is not an ancestor of this branch. The seven archive files are
+vendored in `pinned-export/` and checked by Git blob id. Caller contract on
+this branch: `research/h25-c05-criterion-consumer-contract/ROLE-PROOF.json` and
+`snapshot/original/variant/variant_driver_v1.py.txt` from PR #6397.
+
+### What is proved
+
+The public `verify.py` mentions `original_source_condition_assumptions` once,
+and that occurrence is
+
+```text
+need(len(fixture['original_source_condition_assumptions']) == 56, 'assumption count differs')
+```
+
+So the public PASS authenticates the key count only. Replaying the vendored
+checker on the unmodified archive returns PASS with
+`original_commands_executed = 0`. Replacing `__GNUC_MINOR__` with `4` and
+rewriting the manifest hash leaves that PASS object unchanged. Deleting
+`HAVE_IEEEFP_H` makes the same checker fail with `assumption count differs`.
+That is a proof about this finite program, plus one positive replay, one
+value-changed replay, and one rejection control. It is not a search.
+
+### Exhaustive census of the 56 names
+
+The object has 20 integers and 36 nulls. Neither role's argv contains any of
+the 56 names as an element. The only token agreements are:
+
+| Name | Recorded | Agreement visible in the frozen argv |
+|---|---:|---|
+| `__GNUC__` | 13 | `argv[0]` ends with `x86_64-linux-gnu-gcc-13` |
+| `__STDC_VERSION__` | 201112 | the element `-std=c11` is present |
+
+Those two agreements are spellings in the driver. They are not an installed
+`-dM` dump, and the public replay does not read them. Every other recorded
+integer is absent from the argv. That includes `__GNUC_MINOR__ = 3` and
+`__GNUC_PATCHLEVEL__ = 0`: the basename `gcc-13` does not state the minor or
+the patch.
+
+Recorded integers with no argv element: `_LP64 = 1`, `__CHAR_BIT__ = 8`,
+`__ELF__ = 1`, `__GNUC_MINOR__ = 3`, `__GNUC_PATCHLEVEL__ = 0`, `__LP64__ = 1`,
+`__SIZEOF_LONG__ = 8`, `__SIZEOF_POINTER__ = 8`, `__STDC_HOSTED__ = 1`,
+`__STDC__ = 1`, `__amd64 = 1`, `__amd64__ = 1`, `__gnu_linux__ = 1`,
+`__linux = 1`, `__linux__ = 1`, `__unix__ = 1`, `__x86_64 = 1`,
+`__x86_64__ = 1`.
+
+Recorded nulls, also not argv elements: `HAVE_IEEEFP_H`, `HAVE_STAT_H`,
+`HAVE_SYS_TERMIO_H`, `MS_WINDOWS`, `MS_WINDOWS_DESKTOP`, `MS_WINDOWS_GAMES`,
+`NT_THREADS`, `_AIX`, `_MSC_VER`, `_WIN32`, `_WIN64`, `__ANDROID__`,
+`__APPLE__`, `__CYGWIN__`, `__DragonFly__`, `__FreeBSD__`,
+`__FreeBSD_kernel__`, `__GNU__`, `__HAIKU__`, `__ILP32__`, `__MACH__`,
+`__NetBSD__`, `__OpenBSD__`, `__VMS`, `__VXWORKS__`, `__cplusplus`, `__hpux`,
+`__hpux__`, `__i386`, `__i386__`, `__rtems__`, `__sgi`, `__sun`, `__sun__`,
+`__vxworks`, `__wasi__`.
+
+The frozen commands, reconstructed from the driver and matched to #6397's
+`ROLE-PROOF.json`, are the same in both Python modes:
+
+```text
+/usr/bin/x86_64-linux-gnu-gcc-13 -nostartfiles -shared -fPIC -O3 -std=c11
+  -Wall -Wextra -Werror -I/usr/include/python3.12
+  {S}/areas/field-negative-variants-v1/<role>/dict_probe_fields_v1.c
+  -o {O}/<role>/_h25_dict_probe.cpython-312-x86_64-linux-gnu.so
+```
+
+`<role>` is `pyinit_failure`, then `exec_failure`. There is no `-dM`, `-D`,
+`-U`, `-undef`, or `-include`.
+
+### Hosted implicit include
+
+`/usr/include/stdc-predef.h` is a regular baseline node of 2,462 bytes, mode
+420, sha256
+`8db4f65e62cade8ae4d9b77960ee6aee093255acc1b637e3fb37d79179733b15`. The pinned
+walker resolves that literal path to itself. The public verifier never names
+`stdc-predef`, and none of the 56 keys names it. Presence of the node is not
+a binding of the hosted implicit-include policy. The export's first remaining
+obligation still asks for that binding. The earlier rule model in
+`research/h25-c05-v03-input-constructors/implementation/c05_gcc_rules_v1.py`
+already records `automatic_preinclude.effective = False`; this package does
+not rerun that derivation.
+
+### What this does not show
+
+A null record is not a proof that a header macro is absent after inclusion.
+Both `pyconfig.h` rows are in the graph as regular files with hashes only.
+`SOURCE_MAP.json` excludes original host file contents, so `HAVE_STAT_H = null`
+cannot be compared with those headers here. No installed compiler was run.
+The census is exhaustive for this 56-key object and these two argvs. It is
+not a statement about every GCC invocation. The public graph replay's PASS is
+left intact; only its silence on assumption values is established.
+
+## Reproduce
+
+From the repository root, Python 3.12:
+
+```sh
+python3 -B research/v02-assumption-binding-gap/verify.py
+```
+
+Expected stdout status: `PASS_V02_ASSUMPTION_VALUES_UNBOUND`. The command
+reruns the vendored public checker three times in a temporary directory. It
+does not write the package, open a network connection, or invoke GCC. Pins
+and hashes are in [SOURCES.json](SOURCES.json). The selected-record and
+catalogue rows there are provenance for the card, not inputs of the census.
+
+## Open next questions
+
+1. Can a transcript of these two frozen argvs, with the sample phase named,
+   bind each of the 56 values?
+   *Why:* the public PASS does not. A predefine dump, a dump after
+   `stdc-predef.h`, and a dump after `pyconfig.h` are different claims.
+   *First step:* archive one stdout whose argv equals the frozen command and
+   whose phase is stated, then compare each name.
+   *Blocked by:* the export has no such transcript, host file contents are
+   excluded, and this package does not run a compiler.
+
+2. Do the two hashed `pyconfig.h` rows define `HAVE_STAT_H`, `HAVE_IEEEFP_H`,
+   `HAVE_SYS_TERMIO_H`, `MS_WINDOWS`, `MS_WINDOWS_DESKTOP`,
+   `MS_WINDOWS_GAMES`, or `NT_THREADS`?
+   *Why:* the recorded nulls are compatible both with a predefine-phase sample
+   and with those names never being set. The hashes are
+   `dcda0cfa3f4971db195817881c58025db6c76f19ae45f26d3dda0a43001253e8` and
+   `23931f53bc7ee512c6bd3162828747494eaa5e21f23dd63b31170ec1adfbe65e`.
+   *First step:* compare those hashes to file text that defines or does not
+   define each name.
+   *Blocked by:* the fixture stores the hashes and not the text.
+
+## Credit
+
+The export and the handoff are Chris R / Clear1nsight, PR #7136, with the
+assistance disclosed there. The two-command contract is PR #6397. The
+implicit-include rule left open by the v03 constructor model is that earlier
+package's. Prepared by unpaidmoon with substantial Cursor Grok assistance.
+Apache-2.0.

research/v02-assumption-binding-gap/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
+      "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/h25-c05-criterion-consumer-contract/ROLE-PROOF.json",
+      "usage": "input",
+      "git_blob": "1eb60fe68c0dbb57692e3c2edc5cd30795430698",
+      "sha256": "4f34211c2d72e48c898eaa6033611cd0f22aa12ab15136e5ba2fef5c3d820c73"
+    },
+    {
+      "path": "research/h25-c05-criterion-consumer-contract/snapshot/original/variant/variant_driver_v1.py.txt",
+      "usage": "input",
+      "git_blob": "bfd9b735f6777e99f3adeedd126ab3ce54bce596",
+      "sha256": "cdb1479253358508088f8aa0e1e92e6c75ffcc127e54552698598a02de061254"
+    }
+  ]
+}

research/v02-assumption-binding-gap/TASK.json

@@ -0,0 +1,101 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 8,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "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": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "The 56 original_source_condition_assumptions in the pinned PR #7136 V02 export are not bound by that export's public replay or by the frozen #6397 two-command argv. No selected-frontier assumption is discharged and kappa is unchanged.",
+  "scope_change_reason": "The live #1166 request is the V02 assumption table and the pyinit_failure/exec_failure commands, not a Lean formalization and not one of the five selected assumptions. The card's interface-binding question is kept only as the catalogue provenance.",
+  "bottleneck_link": "Side result. These 56 facts are a named V02 prerequisite, not a selected-invoice term. Showing that the public PASS does not bind them stops a false transfer into the two-role contract; it does not raise kappa.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the public checker is shown to authenticate only the key count, each of the 56 names is compared with the frozen argv, and the stdc-predef node is shown to be unbound. Do not run a compiler or fetch a private archive.",
+  "outcome": "negative-result",
+  "evidence": "verify.py: Git blob ids of the seven vendored export files; the single public assumption predicate is the length check; unmodified PASS, PASS unchanged when __GNUC_MINOR__ becomes 4, and rejection when HAVE_IEEEFP_H is deleted; exhaustive 56-name argv census with two token agreements only; stdc-predef.h resolves as a graph node and is not named by the public checker. No compiler execution.",
+  "author": "unpaidmoon",
+  "ai_assistance": "substantial Cursor Grok assistance",
+  "open_questions": [
+    {
+      "question": "Can a transcript of the two frozen argvs, with the sample phase named, bind each of the 56 values?",
+      "why_it_matters": "The public PASS does not. A predefine dump, a dump after stdc-predef.h, and a dump after pyconfig.h are different claims.",
+      "first_step": "Archive one stdout whose argv equals the frozen command and whose phase is stated, then compare each name.",
+      "blocked_by": "The export has no such transcript, host file contents are excluded, and this package does not run a compiler."
+    },
+    {
+      "question": "Do the two hashed pyconfig.h rows define HAVE_STAT_H, HAVE_IEEEFP_H, HAVE_SYS_TERMIO_H, MS_WINDOWS, MS_WINDOWS_DESKTOP, MS_WINDOWS_GAMES, or NT_THREADS?",
+      "why_it_matters": "The recorded nulls are compatible both with a predefine-phase sample and with those names never being set.",
+      "first_step": "Compare sha256 dcda0cfa3f4971db195817881c58025db6c76f19ae45f26d3dda0a43001253e8 and 23931f53bc7ee512c6bd3162828747494eaa5e21f23dd63b31170ec1adfbe65e to file text.",
+      "blocked_by": "The fixture stores the hashes and not the text."
+    }
+  ]
+}

research/v02-assumption-binding-gap/VERIFY.json

@@ -0,0 +1,21 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/h25-c05-criterion-consumer-contract/ROLE-PROOF.json",
+    "research/h25-c05-criterion-consumer-contract/snapshot/original/variant/variant_driver_v1.py.txt"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Vendored export blob ids, the single length predicate, unmodified public PASS, PASS unchanged when __GNUC_MINOR__ becomes 4, rejection when HAVE_IEEEFP_H is deleted, 56-name argv census, and the unbound stdc-predef.h node. No compiler and no kappa change."
+    }
+  ]
+}