Fail closed on formal CI pipeline errors; bind agent release instructions

.github/workflows/formal-verification.yml

@@ -11,17 +11,22 @@ on:
       - 'formal/**'
       - 'tools/formal_gate_check.py'
       - 'tests/test_formal_gate.py'
+      - 'tests/test_formal_workflow_shell.py'
       - '.github/workflows/formal-verification.yml'
   push:
     branches: [main]
     paths:
       - 'formal/**'
       - 'tools/formal_gate_check.py'
       - 'tests/test_formal_gate.py'
+      - 'tests/test_formal_workflow_shell.py'
       - '.github/workflows/formal-verification.yml'
   workflow_dispatch:
 permissions:
   contents: read
+defaults:
+  run:
+    shell: bash
 jobs:
   kernel-check:
     name: kernel-check
@@ -34,6 +39,19 @@ jobs:
       - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97
         with:
           python-version: '3.11'
+      - name: Verify actual shell rejects a failing producer
+        run: |
+          set +e
+          python -c 'raise SystemExit(17)' | tee "$RUNNER_TEMP/formal-shell-negative.log"
+          status=$?
+          set -e
+          if [ "$status" -ne 17 ]; then
+            echo "PIPELINE_FAILURE_PROPAGATION_FAIL: expected 17, got $status"
+            exit 1
+          fi
+          echo 'PIPELINE_FAILURE_PROPAGATION_PASS'
+      - name: Shell regression controls
+        run: python -B -S -m unittest discover -s tests -p test_formal_workflow_shell.py -v
       - name: Source-only identity gate (no Lean yet; fails closed before any download)
         run: python -B -S tools/formal_gate_check.py
       - name: Install elan (pinned release script, digest checked) and the pinned toolchain
@@ -64,7 +82,11 @@ jobs:
       - name: Describe coverage
         if: always()
         run: |
-          echo 'Kernel evidence for exactly the targets in formal/manifest.json at the checked commit: build, leanchecker, transitive axiom audit (propext / Classical.choice / Quot.sound only), executable negative controls, receipt. Formal evidence only: no Layer 0 review outcome, STATUS row, theorem acceptance, or manifest status was established or changed.' >> "$GITHUB_STEP_SUMMARY"
+          if [ "${{ job.status }}" = "success" ] && [ -s formal/.lake/formal-evidence/receipt.json ]; then
+            echo 'Kernel evidence for exactly the targets in formal/manifest.json at the checked commit: build, leanchecker, transitive axiom audit, executable negative controls, receipt. Formal evidence only: no Layer 0 status or scientific acceptance changed.' >> "$GITHUB_STEP_SUMMARY"
+          else
+            echo 'No successful kernel-verification claim is made for this run. Inspect preserved failures and the actual receipt/logs; neither an artifact nor this summary establishes acceptance.' >> "$GITHUB_STEP_SUMMARY"
+          fi
       - name: Preserve actual results including failures
         if: always()
         uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a

AGENTS.md

@@ -58,3 +58,17 @@ carriers; compiler changes are explicit successors. Review the exact current hea
 and record actual author/reviewer lineage. Do not credit an unobserved reviewer or
 assume that a prior source-bound review remains valid after its source or scope
 changes.
+
+## Release operations and concurrent integration
+
+Read [release operations](docs/RELEASE_OPERATIONS.md) before downloading source,
+provisioning tools or merging. Its snapshots are as-of exact-commit custody, not
+full Git history, LFS or submodule hydration, and a hosted tool receipt is not a
+laptop installation. Keep source and execution repository identities separate.
+
+Re-read the latest source-bound review comments immediately before a merge. A
+known unresolved engineering failure is not discharged by a same-provider review,
+old passing checks, another agent's merge, or a source change outside its review
+scope. Record the actual disposition in the existing PR and main #95. A repair
+claim needs the original failing probe to reject and the amended exact head to
+pass; do not bypass a known failure to make the queue appear empty.

tests/test_formal_workflow_shell.py

@@ -0,0 +1,61 @@
+"""Regression controls for the actual formal workflow shell and failure summary."""
+import os
+from pathlib import Path
+import re
+import subprocess
+import tempfile
+import textwrap
+import unittest
+
+WORKFLOW = Path(__file__).resolve().parents[1] / '.github/workflows/formal-verification.yml'
+PROBE_NAME = 'Verify actual shell rejects a failing producer'
+
+
+def probe_body(text):
+    pattern = r'      - name: ' + re.escape(PROBE_NAME) + r'\n        run: \|\n((?:          [^\n]*\n)+)'
+    found = re.search(pattern, text)
+    if found is None:
+        raise ValueError('missing actual-shell negative control')
+    return textwrap.dedent(found.group(1))
+
+
+class FormalWorkflowShellTests(unittest.TestCase):
+    def setUp(self):
+        self.text = WORKFLOW.read_text()
+
+    def test_explicit_bash_default_without_overrides(self):
+        self.assertIn('defaults:\n  run:\n    shell: bash\n', self.text)
+        self.assertEqual(re.findall(r'^\s+shell:\s*(.+)$', self.text, re.MULTILINE), ['bash'])
+
+    def test_workflow_triggers_and_executes_regression(self):
+        self.assertEqual(self.text.count("      - 'tests/test_formal_workflow_shell.py'"), 2)
+        self.assertIn('python -B -S -m unittest discover -s tests -p test_formal_workflow_shell.py -v', self.text)
+
+    def run_probe(self, pipefail):
+        body = probe_body(self.text)
+        with tempfile.TemporaryDirectory() as tmp:
+            script = Path(tmp)/'probe.sh'; script.write_text(body)
+            cmd = ['bash', '--noprofile', '--norc', '-e']
+            if pipefail:
+                cmd += ['-o', 'pipefail']
+            cmd.append(str(script))
+            return subprocess.run(cmd, env={**os.environ, 'RUNNER_TEMP': tmp},
+                                  capture_output=True, text=True, timeout=20)
+
+    def test_actual_probe_accepts_fail_closed_shell(self):
+        result = self.run_probe(True)
+        self.assertEqual(result.returncode, 0, result.stdout+result.stderr)
+        self.assertIn('PIPELINE_FAILURE_PROPAGATION_PASS', result.stdout)
+
+    def test_actual_probe_rejects_original_fail_open_shell(self):
+        result = self.run_probe(False)
+        self.assertNotEqual(result.returncode, 0, result.stdout+result.stderr)
+        self.assertIn('PIPELINE_FAILURE_PROPAGATION_FAIL', result.stdout)
+
+    def test_summary_does_not_claim_success_unconditionally(self):
+        self.assertIn('if [ "${{ job.status }}" = "success" ] && [ -s formal/.lake/formal-evidence/receipt.json ]; then', self.text)
+        self.assertIn('No successful kernel-verification claim is made for this run.', self.text)
+
+
+if __name__ == '__main__':
+    unittest.main()