Finalize RMQ v1.0.0-rc.1

.gitattributes

@@ -29,3 +29,20 @@ docs/internal/extensions/bv1/COORDINATOR_ROUTE_DISPOSITION.md whitespace=blank-a
 docs/internal/extensions/bv1/controls/public_mutations/fixtures/B39CFA73CEAA05B8D0E8E803CACF0696529FDBF7F2BD3BEFB5A8805045127618/*.constructor.lean whitespace=blank-at-eol,-blank-at-eof,space-before-tab,cr-at-eol
 docs/internal/extensions/bv1/controls/public_mutations/snapshots/97405C70ED3B60CED72874D6DF622D2E9BBA0BD8F04808A3F98ED34EE1CEB770/Capstone.lean whitespace=blank-at-eol,-blank-at-eof,space-before-tab,cr-at-eol
 scripts/packed_bitvector_validation_controls.ps1 whitespace=blank-at-eol,-blank-at-eof,space-before-tab,cr-at-eol
+
+# LIFE-NATIVE-1 checks these two frozen artifacts as exact Git bytes (LF).
+# Preserve the contract and complete matrix rows.
+docs/internal/extensions/lifecycle-native1/CONTRACT_REQUIREMENTS.json -text
+docs/internal/extensions/lifecycle-native1/ACCEPTANCE_MATRIX.frozen.md -text
+
+# The semantic fixture registry and startup amendment use historical CRLF hashes.
+# The startup amendment compares against historical Windows raw-source hashes.
+# These two source files must retain that explicit CRLF representation even
+# when a checkout has core.autocrlf disabled. The Lean text is unchanged.
+scripts/lifecycle_native_cases.json text eol=crlf
+RMQ/Core/SuccinctClose/EndpointFringe/InteriorCandidate/InteriorDirectory/SparseLevelWidth.lean text eol=crlf
+RMQ/Core/SuccinctFinal/RAM/ReviewerReachabilitySmall.lean text eol=crlf
+
+# Preserve the two V1 external audit reports as exact recorded bytes.
+docs/internal/audit_reports/v1-blind-4ded05c.md -text whitespace=blank-at-eol,blank-at-eof,space-before-tab,cr-at-eol
+docs/internal/audit_reports/v1-blind-ff92a2f-continuation.md -text whitespace=blank-at-eol,blank-at-eof,space-before-tab,cr-at-eol

.github/workflows/ci.yml

@@ -150,3 +150,19 @@ jobs:
       - name: Owned-process self-test (setsid group + descendant barrier)
         shell: pwsh
         run: ./scripts/owned_process_tree.ps1 -SelfTest
+
+  source-artifact-checks:
+    name: Source artifact checks (${{ matrix.os }})
+    runs-on: ${{ matrix.os }}
+    strategy:
+      matrix:
+        os: [ubuntu-24.04, windows-2022]
+    steps:
+      - name: Checkout
+        uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4
+
+      - name: Packaging integrity and checkout byte regressions
+        shell: bash
+        run: |
+          python scripts/test_package_release.py
+          python scripts/test_native_checkout.py

.github/workflows/release-artifact.yml

@@ -16,7 +16,7 @@ jobs:
       - name: Checkout
         uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4
         with:
-          fetch-depth: 2
+          fetch-depth: 0
           # This workflow also runs scripts/gate.ps1, through
           # scripts/reproduce_artifact.sh, so it needs tags for the same reason
           # ci.yml does. WDD-20260816-057 said "every workflow" and fixed two.
@@ -34,7 +34,7 @@ jobs:
         shell: bash
         run: |
           set -o pipefail
-          scripts/reproduce_artifact.sh 2>&1 | tee artifact-reproduction.log
+          scripts/reproduce_artifact.sh 2>&1 | tee "$RUNNER_TEMP/artifact-reproduction.log"
 
       - name: Prepare release attachments
         shell: bash
@@ -45,7 +45,7 @@ jobs:
             --exclude=.lake \
             --exclude=release-artifacts \
             -czf "release-artifacts/rmq-source-${GITHUB_REF_NAME}.tar.gz" .
-          cp artifact-reproduction.log release-artifacts/
+          cp "$RUNNER_TEMP/artifact-reproduction.log" release-artifacts/
           cp docs/ARTIFACT_REPRODUCIBILITY.md release-artifacts/
           cp docs/PAPER_MAIN_THEOREM.md release-artifacts/
           cp docs/PAPER_THEOREM_MAP.md release-artifacts/
@@ -59,10 +59,14 @@ jobs:
         shell: bash
         run: |
           tag="${GITHUB_REF_NAME}"
+          release_flags=()
+          if [[ "$tag" == *-* ]]; then
+            release_flags+=(--prerelease)
+          fi
           if gh release view "$tag" >/dev/null 2>&1; then
             gh release upload "$tag" release-artifacts/* --clobber
           else
-            gh release create "$tag" release-artifacts/* \
+            gh release create "$tag" release-artifacts/* "${release_flags[@]}" \
               --title "$tag" \
               --notes "RMQ paper artifact release. See ARTIFACT_REPRODUCIBILITY.md and artifact-reproduction.log."
           fi

CITATION.cff

@@ -1,5 +1,5 @@
 cff-version: 1.2.0
-message: "If you use this Lean artifact, please cite it using this provisional metadata."
+message: "If you use this Lean artifact, cite this release-candidate version and the exact source commit. No V1 release has been published yet."
 title: "RMQ: A Lean 4 Artifact for Succinct Range Minimum Query Models"
 type: software
 authors:
@@ -13,5 +13,4 @@ keywords:
   - succinct data structures
   - formal verification
 license: Apache-2.0
-version: "provisional"
-date-released: "2026-07-06"
+version: 1.0.0-rc.1