Audit global bypass reductions for c4 h7

.github/workflows/c4-h7-d2-three-source-past.yml

@@ -0,0 +1,242 @@
+name: Audit c4 h7 three-source zero-debt pasts
+run-name: Exact c4 k2 h7 past restoration and independent initial-state audit
+
+on:
+  push:
+    branches: [codex/c4-h7-global-bypass]
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+concurrency:
+  group: c4-h7-d2-three-source-past-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  formal-past-restoration:
+    runs-on: ubuntu-latest
+    timeout-minutes: 360
+    steps:
+      - uses: actions/checkout@v5
+      - uses: actions/setup-python@v5
+        with:
+          python-version: "3.12"
+
+      - name: Configure and build the two solvers plus certificate tools
+        run: |
+          cmake -S . -B build \
+            -DCMAKE_BUILD_TYPE=Release \
+            -DWSC_WARNINGS_AS_ERRORS=ON
+          cmake --build build \
+            --target \
+              water-c4-h7-d2-three-source \
+              water-c4-h7-d2-three-source-past \
+              water-oracle \
+              water-verify \
+            --parallel 2
+
+      - name: Rebuild the complete 1106490-future checkpoint
+        run: |
+          mkdir -p out/checkpoint
+          set -o pipefail
+          build/water-c4-h7-d2-three-source \
+            --self-test --output-dir out/checkpoint 2>&1 \
+            | tee out/checkpoint/production.log
+          python scripts/validate_c4_h7_d2_three_source_report.py \
+            out/checkpoint/report.json --negative-tests
+
+      - name: Independently reproduce every checkpoint row
+        run: |
+          set -o pipefail
+          python tests/check_c4_h7_d2_three_source.py \
+            --report out/checkpoint/report.json \
+            --json out/checkpoint/independent-audit.json \
+            --local-no-ledger out/checkpoint/independent-local-no-ledger.jsonl 2>&1 \
+            | tee out/checkpoint/independent.log
+
+      - name: Prove the unified all-local-NO bypass symbolically and against the artifact
+        run: |
+          set -o pipefail
+          python tests/check_c4_h7_d2_three_source_all_local_no_bypass.py 2>&1 \
+            | tee out/checkpoint/all-local-no-bypass-symbolic.log
+          python tests/check_c4_h7_d2_three_source_all_local_no_bypass.py \
+            --report out/checkpoint/report.json \
+            --ledger out/checkpoint/local-no-ledger.jsonl 2>&1 \
+            | tee out/checkpoint/all-local-no-bypass-artifact.log
+
+      - name: Verify the sparse early-low continuation kernels
+        run: |
+          set -o pipefail
+          python tests/check_c4_h7_sparse_all_q_continuation.py \
+            --checkpoint-report out/checkpoint/report.json 2>&1 \
+            | tee out/checkpoint/sparse-all-q-continuation.log
+
+      - name: Run a bounded past-restoration row differential first
+        run: |
+          mkdir -p out/past-bounded
+          set -o pipefail
+          build/water-c4-h7-d2-three-source-past \
+            --checkpoint-report out/checkpoint/report.json \
+            --output-dir out/past-bounded \
+            --limit-restorations 64 \
+            --self-test 2>&1 \
+            | tee out/past-bounded/production.log
+          python scripts/validate_c4_h7_d2_three_source_past_report.py \
+            out/past-bounded/report.json --negative-tests
+          python tests/check_c4_h7_d2_three_source_past.py \
+            --checkpoint-report out/checkpoint/report.json \
+            --production-report out/past-bounded/report.json \
+            --limit 64 \
+            --json out/past-bounded/independent-audit.json
+
+      - name: Solve the complete 285600 balanced restoration superset
+        run: |
+          mkdir -p out/past-full
+          set -o pipefail
+          build/water-c4-h7-d2-three-source-past \
+            --checkpoint-report out/checkpoint/report.json \
+            --output-dir out/past-full \
+            --self-test 2>&1 \
+            | tee out/past-full/production.log
+          python scripts/validate_c4_h7_d2_three_source_past_report.py \
+            out/past-full/report.json --negative-tests
+
+      - name: Independently rebuild and compare all restored initial layouts
+        run: |
+          set -o pipefail
+          python tests/check_c4_h7_d2_three_source_past.py \
+            --checkpoint-report out/checkpoint/report.json \
+            --production-report out/past-full/report.json \
+            --full \
+            --json out/past-full/independent-audit.json 2>&1 \
+            | tee out/past-full/independent.log
+
+      - name: Gate all-YES and candidate outcomes at their exact claim boundary
+        run: |
+          python - <<'PY'
+          import json
+          from pathlib import Path
+
+          production = json.loads(Path("out/past-full/report.json").read_text())
+          independent = json.loads(Path("out/past-full/independent-audit.json").read_text())
+          if independent["run"]["row_by_row_agreement"] is not True:
+              raise SystemExit("the independent implementation did not compare every row")
+          if independent["run"]["production_rows_compared"] != 285_600:
+              raise SystemExit("the independent implementation did not cover the full superset")
+          if production["status"] != independent["status"]:
+              raise SystemExit("the two initial-state implementations disagree on status")
+          status = production["status"]
+          if status == "THREE_SOURCE_PAST_FAMILY_ELIMINATED":
+              if production["run"]["initial_no"] != 0:
+                  raise SystemExit("all-YES status contains a NO")
+              if independent["claims"]["restoration_family_eliminated"] is not True:
+                  raise SystemExit("independent implementation did not prove the finite-family result")
+          elif status == "INITIAL_NO_CANDIDATES_EXPORTED":
+              if production["run"]["initial_no"] == 0:
+                  raise SystemExit("candidate status contains no candidate")
+              if independent["run"]["initial_no"] != production["run"]["initial_no"]:
+                  raise SystemExit("the two implementations disagree on candidate count")
+          else:
+              raise SystemExit(f"formal past run ended in unsafe status {status!r}")
+          Path("out/past-full/pre-certificate-status.txt").write_text(status + "\n")
+          PY
+
+      - name: Independently certify any complete-layout NO candidate
+        run: |
+          status="$(cat out/past-full/pre-certificate-status.txt)"
+          if test "$status" = INITIAL_NO_CANDIDATES_EXPORTED; then
+            set -o pipefail
+            build/water-oracle \
+              --input out/past-full/initial-no-candidate.txt \
+              --count 1 \
+              --certificate out/past-full/global-no-candidate.wscert 2>&1 \
+              | tee out/past-full/water-oracle.log
+            grep -Eq '^border_sequences=0([[:space:]]|$)' out/past-full/water-oracle.log
+            grep -Fxq UNSOLVABLE out/past-full/water-oracle.log
+            test -s out/past-full/global-no-candidate.wscert
+            build/water-verify \
+              --input out/past-full/initial-no-candidate.txt \
+              --certificate out/past-full/global-no-candidate.wscert 2>&1 \
+              | tee out/past-full/water-verify.log
+            grep -Fxq 'VALID NO CERTIFICATE' out/past-full/water-verify.log
+          fi
+
+      - name: Emit only the conclusion justified by both implementations
+        run: |
+          python - <<'PY'
+          import hashlib
+          import json
+          from pathlib import Path
+
+          directory = Path("out/past-full")
+          production = json.loads((directory / "report.json").read_text())
+          independent = json.loads((directory / "independent-audit.json").read_text())
+          candidate = production["status"] == "INITIAL_NO_CANDIDATES_EXPORTED"
+          certificate = directory / "global-no-candidate.wscert"
+          if candidate and not certificate.is_file():
+              raise SystemExit("a DP NO was not promoted because no verified certificate exists")
+          status = "GLOBAL_NO_CERTIFIED" if candidate else "THREE_SOURCE_PAST_FAMILY_ELIMINATED"
+          result = {
+              "schema_version": 1,
+              "experiment": "c4_h7_d2_three_source_past_formal_gate",
+              "status": status,
+              "evidence": {
+                  "production_status": production["status"],
+                  "independent_status": independent["status"],
+                  "rows_compared": independent["run"]["production_rows_compared"],
+                  "oracle_count_cap": 1 if candidate else None,
+                  "water_verify_passed": candidate,
+                  "certificate_sha256": hashlib.sha256(certificate.read_bytes()).hexdigest() if candidate else None,
+              },
+              "scope": {
+                  "balanced_restoration_superset": 285_600,
+                  "parent_reachable_subset": 281_904,
+                  "universal_c4_h7_solvability": False,
+              },
+              "claims": {
+                  "three_source_past_family_eliminated": not candidate,
+                  "global_no_certified": candidate,
+                  "universal_c4_h7_solvability": False,
+              },
+          }
+          (directory / "formal-result.json").write_text(json.dumps(result, indent=2, sort_keys=True) + "\n")
+          (directory / "status.txt").write_text(status + "\n")
+          PY
+
+      - name: Record the exact finite-family conclusion
+        if: success()
+        run: |
+          python - <<'PY' >> "$GITHUB_STEP_SUMMARY"
+          import json
+          from pathlib import Path
+
+          result = json.loads(Path("out/past-full/formal-result.json").read_text())
+          if result["status"] == "GLOBAL_NO_CERTIFIED":
+              print(
+                  "> A complete balanced c4/h7 layout from this restoration family is NO: "
+                  "the independent oracle found zero solutions and water-verify accepted its closure certificate."
+              )
+          else:
+              print(
+                  "> Both independent implementations found all 285,600 balanced restorations YES. "
+                  "This eliminates exactly the restored three-source residual family; it is not a universal c4/h7 proof."
+              )
+          PY
+          cat out/past-full/report.md >> "$GITHUB_STEP_SUMMARY"
+
+      - name: Create and verify the evidence manifest
+        if: always()
+        run: |
+          find out -type f ! -name SHA256SUMS -print0 \
+            | sort -z \
+            | xargs -0 -r sha256sum > out/SHA256SUMS
+          sha256sum --check out/SHA256SUMS
+
+      - uses: actions/upload-artifact@v6
+        if: always()
+        with:
+          name: c4-h7-d2-three-source-past-${{ github.run_id }}
+          path: out/
+          if-no-files-found: error
+          retention-days: 30