From c7a0250b389718126984834203b2a7832cf7257e Mon Sep 17 00:00:00 2001 From: Dylan Roy Date: Sun, 27 Sep 2026 17:42:42 -0500 Subject: [PATCH] Make formal CI pipelines fail closed and link release operations Narrow repair for AMEND5332434827 left unresolved when peer PR181 merged. Explicit Bash/pipefail default, actual-shell failing-producer control, five test-first regressions passing in normal/-O modes, conditional coverage summary. Append current/future-agent release instructions. No Lean statement, manifest, scientific status or historical receipt changed. --- .github/workflows/formal-verification.yml | 24 ++++++++- AGENTS.md | 14 ++++++ tests/test_formal_workflow_shell.py | 61 +++++++++++++++++++++++ 3 files changed, 98 insertions(+), 1 deletion(-) create mode 100644 tests/test_formal_workflow_shell.py diff --git a/.github/workflows/formal-verification.yml b/.github/workflows/formal-verification.yml index 315f82d50..0a1076052 100644 --- a/.github/workflows/formal-verification.yml +++ b/.github/workflows/formal-verification.yml @@ -11,6 +11,7 @@ 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] @@ -18,10 +19,14 @@ on: - '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 diff --git a/AGENTS.md b/AGENTS.md index d88057a98..ba2c59305 100644 --- a/AGENTS.md +++ b/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. diff --git a/tests/test_formal_workflow_shell.py b/tests/test_formal_workflow_shell.py new file mode 100644 index 000000000..3d7a459bb --- /dev/null +++ b/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()