CI: build the XMSS Lean formalization as a required check

[alexanderlhicks]

The XMSS root theorem has useful axiom-footprint guards, but neither repository workflow builds formal/xmss. A guard in XmssSecurity.lean protects the theorem only when that module is elaborated.

This is currently observable in the workflows at the PR 10 merge: Rust and the two PDFs are checked, but lake build is not run. The formal project itself builds successfully with the pinned Lean 4.31.0 toolchain and VCVio manifest.

Please add a required clean-runner job that installs the toolchain from formal/xmss/lean-toolchain and runs:

cd formal/xmss
lake build

The checked-in manifest should be used as-is rather than updated in CI. A source-wide forbidden-token scan and archived #print axioms output would be useful defense in depth. For new modules, set_option autoImplicit false would also catch misspelled free identifiers becoming unintended theorem parameters; existing modules can be migrated or audited incrementally.

Acceptance criteria:

• A clean CI runner builds the default XmssSecurity target.
• The two root #guard_msgs checks execute.
• The job is required before future formalization or XMSS-document changes merge.

AI assistance disclosure: this issue was prepared with help from an OpenAI Codex agent during a fresh adversarial review of PR 10. The agent was instructed to reproduce or otherwise evidence each finding, try to falsify it, distinguish PR changes from pre-existing and later mainline changes, and make the proposed resolution pedagogical and actionable. The evidence in this issue was rechecked against merged commit f5d6e5040d666981005371742a6f21640ce865a1.

[alexanderlhicks]

Proposed fix

This is the issue-specific patch currently prepared in a local working tree based on f5d6e5040d666981005371742a6f21640ce865a1. It has not been committed or pushed.

The invariant we need is simple: every pull request must elaborate the default XmssSecurity target, because the theorem's axiom guards only execute when the root module is built. The job belongs in an unfiltered workflow so it is always present and can safely become a required check.

Exact diff

diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml
index d999608..d96b7c0 100644
--- a/.github/workflows/rust.yml
+++ b/.github/workflows/rust.yml
@@ -14,6 +14,18 @@ concurrency:
   cancel-in-progress: true
 
 jobs:
+  xmss-formalization:
+    name: XMSS formalization
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: leanprover/lean-action@v1
+        with:
+          lake-package-directory: formal/xmss
+          build: true
+          test: false
+          lint: false
+
   release:
     runs-on: ubuntu-latest
     steps:

Why this shape

• leanprover/lean-action@v1 is the official Lean CI action and supports a Lake package in a repository subdirectory through lake-package-directory.
• build: true makes the required operation explicit instead of relying only on automatic target detection.
• test: false and lint: false accurately reflect this package: its acceptance condition is elaboration of the default library target and the root #guard_msgs, not a separate Lake test or lint driver.
• Reusing the existing pull-request workflow matches repository style, inherits its read-only contents permission, and avoids the required-check problem caused by path-filtered workflows that do not run on every PR.
• The action reads formal/xmss/lean-toolchain and lake-manifest.json; the proposal does not update dependency revisions in CI.

Validation

Equivalent local clean-runner commands were executed from formal/xmss:

$ lake exe cache get
Completed successfully

$ lake build
✔ [2866/2867] Built XmssSecurity
Build completed successfully (2867 jobs).

Additional checks:

$ ruby -e 'require "yaml"; YAML.parse_file(".github/workflows/rust.yml")'
workflow YAML parses

$ git diff --check
# no output, exit 0

git status after the build confirms that neither lake-manifest.json nor any formal source changed. The GitHub-hosted action itself cannot execute until the patch is pushed, but the same package path, manifest, toolchain, and lake build command have completed locally.

The fenced diff was extracted verbatim and git apply --check accepted it against f5d6e5040d666981005371742a6f21640ce865a1.

Compatibility and remaining step

This changes CI only; it does not change Lean, Rust, the proof statement, or the dependency lock. After the patch is pushed and the job has run once, branch protection still has to mark Rust / XMSS formalization as required. A workflow file can create the check but cannot make itself mandatory.

AI assistance disclosure: this proposed patch and validation report were prepared with help from an OpenAI Codex agent. The agent was asked to review the exact diff as if it were a focused PR, check repository and workflow conventions, execute the equivalent clean build, state what was not locally reproducible, and avoid overstating branch-protection coverage.