proofs(octad): mechanise octad modality algebra (O-series + R1–R3)

.clusterfuzzlite/build.sh

@@ -12,20 +12,48 @@
 
 set -euo pipefail
 
+# ── Toolchain floor ──────────────────────────────────────────────────────
+# The OSS-Fuzz base-builder-rust image pins an older nightly (rustc 1.91 at
+# time of writing), but part of the dependency graph — burn / cubecl-zspace,
+# pulled transitively via verisim-tensor (fuzz -> verisim-api) —
+# declares rust-version = 1.92. cargo-fuzz rebuilds the standard library with
+# -Zbuild-std, so all we need is a new-enough nightly with rust-src present.
+# Install one and force it for the whole script via RUSTUP_TOOLCHAIN. This is
+# contained to the fuzz job: it never touches the main workspace toolchain or
+# any other CI job.
+rustup toolchain install nightly --profile minimal \
+    --component rust-src --component llvm-tools-preview
+export RUSTUP_TOOLCHAIN=nightly
+
 # cargo-fuzz drives libfuzzer; install it if missing.
 if ! command -v cargo-fuzz &>/dev/null; then
     cargo install cargo-fuzz --locked
 fi
 
-# ── fuzz_octad_id — top-level fuzz crate ─────────────────────────────────
-cd "${SRC}/verisimdb/fuzz"
-cargo fuzz build --release --sanitizer="${SANITIZER:-address}"
-cp target/*/release/fuzz_octad_id "${OUT}/"
+# Build one named fuzz target from the project's single cargo-fuzz crate
+# (fuzz/) and copy the binary to $OUT. cargo-fuzz resolves ONE fuzz directory
+# per project, so both targets are hosted in fuzz/; building each by name is
+# reliable. We then locate the produced binary wherever cargo-fuzz placed it
+# (not a brittle glob), failing loudly if nothing was produced.
+build_target() {
+    local crate_dir="$1" target="$2"
+    echo "── building fuzz target '${target}' in ${crate_dir} ──"
+    (
+        cd "${crate_dir}"
+        cargo fuzz build --release --sanitizer="${SANITIZER:-address}" "${target}"
+        local bin
+        bin="$(find . -type f -name "${target}" -path '*/release/*' -print -quit)"
+        if [[ -z "${bin}" ]]; then
+            echo "ERROR: no '${target}' binary produced under ${crate_dir}" >&2
+            exit 1
+        fi
+        cp "${bin}" "${OUT}/${target}"
+        echo "── copied ${bin} -> ${OUT}/${target} ──"
+    )
+}
 
-# ── fuzz_vql_parser — rust-core fuzz crate ───────────────────────────────
-cd "${SRC}/verisimdb/rust-core/fuzz"
-cargo fuzz build --release --sanitizer="${SANITIZER:-address}"
-cp target/*/release/fuzz_vql_parser "${OUT}/"
+build_target "${SRC}/verisimdb/fuzz" fuzz_octad_id
+build_target "${SRC}/verisimdb/fuzz" fuzz_vql_parser
 
 # Optional seed corpora — empty for now, will populate as we discover
 # interesting inputs.  Comment in once corpora exist:

.github/workflows/build-validation.yml

@@ -15,9 +15,9 @@ jobs:
     name: Rust build validation
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v6.0.3
-      - uses: dtolnay/rust-toolchain@stable
-      - uses: Swatinem/rust-cache@v2
+      - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
+      - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
+      - uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
       - run: cargo check --workspace
 
   validate-elixir:
@@ -27,8 +27,8 @@ jobs:
       run:
         working-directory: elixir-orchestration
     steps:
-      - uses: actions/checkout@v6.0.3
-      - uses: erlef/setup-beam@v1
+      - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
+      - uses: erlef/setup-beam@8251c48667b97e88a0a24ec512f5b72a039fcea7 # v1
         with:
           elixir-version: "1.17"
           otp-version: "27"

.github/workflows/coq-build.yml

@@ -90,6 +90,12 @@ jobs:
           set -euo pipefail
           coqc -q PlannerSemantic.v | tee PlannerSemantic.out
 
+      - name: Compile Octad.v
+        working-directory: formal
+        run: |
+          set -euo pipefail
+          coqc -q Octad.v | tee Octad.out
+
       - name: Verify Provenance assumptions whitelist
         working-directory: formal
         run: |
@@ -220,3 +226,22 @@ jobs:
             exit 1
           fi
           echo "OK(PlannerSemantic): Q1-full semantic equivalence + membership"
+
+      - name: Verify Octad assumptions whitelist
+        working-directory: formal
+        run: |
+          set -euo pipefail
+          # Whitelist: 2 Parameters (mval, ident) + functional_extensionality_dep
+          # (Coq stdlib). modality is inductive; resolve is an operation
+          # argument — neither is an axiom.
+          UNEXPECTED=$(awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Octad.out \
+            | sort -u \
+            | grep -vE '^(mval|ident|functional_extensionality_dep)$' || true)
+          if [ -n "$UNEXPECTED" ]; then
+            echo "ERROR(Octad): unexpected axiom(s) in Print Assumptions:"
+            echo "$UNEXPECTED"
+            echo "---"
+            cat Octad.out
+            exit 1
+          fi
+          echo "OK(Octad): O-series + R1-R3 modality algebra whitelisted"

.github/workflows/fuzz.yml

@@ -25,9 +25,9 @@ jobs:
     permissions:
       contents: read
     steps:
-      - uses: actions/checkout@v6.0.3
-      - uses: dtolnay/rust-toolchain@stable
-      - uses: Swatinem/rust-cache@v2
+      - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
+      - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
+      - uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
       - name: Run core fuzz compile check
         run: |
           cd rust-core/fuzz
@@ -40,9 +40,9 @@ jobs:
     permissions:
       contents: read
     steps:
-      - uses: actions/checkout@v6.0.3
-      - uses: dtolnay/rust-toolchain@stable
-      - uses: Swatinem/rust-cache@v2
+      - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
+      - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
+      - uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
       - name: Run debugger fuzz compile check
         run: |
           cd debugger/fuzz

.github/workflows/rust-ci.yml

@@ -28,8 +28,8 @@ jobs:
     name: rustfmt
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v6.0.3
-      - uses: dtolnay/rust-toolchain@stable
+      - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
+      - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
         with:
           components: rustfmt
       - run: cargo fmt --all -- --check
@@ -38,20 +38,20 @@ jobs:
     name: clippy (all-targets)
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v6.0.3
-      - uses: dtolnay/rust-toolchain@stable
+      - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
+      - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
         with:
           components: clippy
-      - uses: Swatinem/rust-cache@v2
+      - uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
       - run: cargo clippy --workspace --all-targets --no-deps -- -D warnings
 
   test:
     name: cargo test
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v6.0.3
-      - uses: dtolnay/rust-toolchain@stable
-      - uses: Swatinem/rust-cache@v2
+      - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
+      - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
+      - uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
       - run: cargo test --workspace --no-fail-fast
 
   doc:
@@ -60,51 +60,51 @@ jobs:
     env:
       RUSTDOCFLAGS: "-D warnings"
     steps:
-      - uses: actions/checkout@v6.0.3
-      - uses: dtolnay/rust-toolchain@stable
-      - uses: Swatinem/rust-cache@v2
+      - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
+      - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
+      - uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
       - run: cargo doc --workspace --no-deps
 
   audit:
     name: cargo audit
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v6.0.3
-      - uses: rustsec/audit-check@v2.0.0
+      - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
+      - uses: rustsec/audit-check@69366f33c96575abad1ee0dba8212993eecbe998 # v2.0.0
         with:
           token: ${{ secrets.GITHUB_TOKEN }}
 
   deny:
     name: cargo deny
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v6.0.3
-      - uses: EmbarkStudios/cargo-deny-action@v2
+      - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
+      - uses: EmbarkStudios/cargo-deny-action@8f84122a46a358a27cb0625d85ad60ab436a1b87 # v2
         with:
           command: check advisories bans licenses sources
 
   bench-compile:
     name: benchmarks compile
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v6.0.3
-      - uses: dtolnay/rust-toolchain@stable
-      - uses: Swatinem/rust-cache@v2
+      - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
+      - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
+      - uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
       - run: cargo bench --no-run
 
   coverage:
     name: cargo-llvm-cov (≥60%)
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v6.0.3
-      - uses: dtolnay/rust-toolchain@stable
+      - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
+      - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
         with:
           components: llvm-tools-preview
-      - uses: Swatinem/rust-cache@v2
-      - uses: taiki-e/install-action@cargo-llvm-cov
+      - uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
+      - uses: taiki-e/install-action@28ba36d36bfc4814f98a469ff9f76b2a41e9aa8a # cargo-llvm-cov
       - name: Generate lcov report
         run: cargo llvm-cov --workspace --lcov --output-path lcov.info
-      - uses: codecov/codecov-action@v6
+      - uses: codecov/codecov-action@e79a6962e0d4c0c17b229090214935d2e33f8354 # v6
         with:
           files: lcov.info
           flags: rust
@@ -122,10 +122,10 @@ jobs:
     runs-on: ubuntu-latest
     if: github.event_name == 'workflow_dispatch' || github.event_name == 'schedule'
     steps:
-      - uses: actions/checkout@v6.0.3
-      - uses: dtolnay/rust-toolchain@stable
-      - uses: Swatinem/rust-cache@v2
-      - uses: taiki-e/install-action@v2
+      - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
+      - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
+      - uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
+      - uses: taiki-e/install-action@25435dc8dd3baed7417e0c96d3fe89013a5b2e09 # v2
         with:
           tool: cargo-mutants
       - name: Run mutation tests on core invariant crates
@@ -140,7 +140,7 @@ jobs:
             --no-shuffle \
             --output mutants-out/
         continue-on-error: true
-      - uses: actions/upload-artifact@v7
+      - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7
         if: always()
         with:
           name: mutants-report
@@ -155,7 +155,7 @@ jobs:
           - fuzz/Cargo.toml
           - rust-core/fuzz/Cargo.toml
     steps:
-      - uses: actions/checkout@v6.0.3
-      - uses: dtolnay/rust-toolchain@stable
-      - uses: Swatinem/rust-cache@v2
+      - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3
+      - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable
+      - uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2
       - run: cargo check --manifest-path ${{ matrix.manifest }}