bundle-push.yml

name: Bundle Push

on:
  push:
    tags:
      - "v*"
  workflow_dispatch:
    inputs:
      version:
        description: "Version to bundle (e.g., v1.0.0)"
        required: true
        default: "v0.1.0"

jobs:
  create-bundle:
    runs-on: ubuntu-latest
    permissions:
      contents: read
      id-token: write

    steps:
      - name: Checkout code
        uses: actions/checkout@v4

      - name: Setup Lean 4
        uses: leanprover/lean-action@v1

      - name: Setup Rust
        uses: dtolnay/rust-toolchain@stable

      - name: Cache dependencies
        uses: actions/cache@v4
        with:
          path: |
            ~/.cargo/registry
            ~/.cargo/git
            .lake
          key: ${{ runner.os }}-bundle-${{ hashFiles('lakefile.lean', 'src/rust/guardd/Cargo.toml') }}
          restore-keys: |
            ${{ runner.os }}-bundle-

      - name: Build components
        run: |
          echo "Building Lean components..."
          lake build

          echo "Building Rust components..."
          cargo build --release --manifest-path src/rust/guardd/Cargo.toml

      - name: Create bundle
        run: |
          echo "Creating Model Asset Guard bundle..."

          # Determine version
          if [ "${{ github.event_name }}" = "workflow_dispatch" ]; then
            VERSION="${{ github.event.inputs.version }}"
          else
            VERSION="${GITHUB_REF#refs/tags/}"
          fi

          echo "Creating bundle for version: $VERSION"

          # Create bundle directory
          BUNDLE_DIR="model-asset-guard-$VERSION"
          mkdir -p "$BUNDLE_DIR"

          # Copy specification files
          echo "Copying specification files..."
          mkdir -p "$BUNDLE_DIR/Spec"
          cp src/lean/ModelAssetGuard/Weights.lean "$BUNDLE_DIR/Spec/" 2>/dev/null || echo "Weights.lean not found"
          cp src/lean/ModelAssetGuard/Quant/Core.lean "$BUNDLE_DIR/Spec/" 2>/dev/null || echo "Core.lean not found"
          cp src/lean/ModelAssetGuard/Quant/LayerBound.lean "$BUNDLE_DIR/Spec/" 2>/dev/null || echo "LayerBound.lean not found"
          cp src/lean/ModelAssetGuard/Token/Tokenizer.lean "$BUNDLE_DIR/Spec/" 2>/dev/null || echo "Tokenizer.lean not found"

          # Copy bindings
          echo "Copying language bindings..."
          mkdir -p "$BUNDLE_DIR/bindings"
          cp bindings/python/pytorch_guard.py "$BUNDLE_DIR/bindings/" 2>/dev/null || echo "pytorch_guard.py not found"
          cp bindings/nodejs/node_guard.js "$BUNDLE_DIR/bindings/" 2>/dev/null || echo "node_guard.js not found"

          # Copy Rust library
          echo "Copying Rust library..."
          mkdir -p "$BUNDLE_DIR/guardd"
          if [ -f "src/rust/guardd/target/release/libguardd.so" ]; then
            cp src/rust/guardd/target/release/libguardd.so "$BUNDLE_DIR/guardd/"
          elif [ -f "src/rust/guardd/target/release/guardd.dll" ]; then
            cp src/rust/guardd/target/release/guardd.dll "$BUNDLE_DIR/guardd/"
          elif [ -f "src/rust/guardd/target/release/libguardd.dylib" ]; then
            cp src/rust/guardd/target/release/libguardd.dylib "$BUNDLE_DIR/guardd/"
          else
            echo "Warning: No Rust library found"
          fi

          # Copy configuration files
          echo "Copying configuration files..."
          cp lakefile.lean "$BUNDLE_DIR/"
          cp lean-toolchain "$BUNDLE_DIR/"
          cp LICENSE "$BUNDLE_DIR/"

          # Generate Lean kernel hash
          echo "Generating Lean kernel hash..."
          KERNEL_HASH=$(lake exe lean --version 2>/dev/null | head -1 | sha256sum | cut -d' ' -f1)
          echo "$KERNEL_HASH" > "$BUNDLE_DIR/lean-hash.txt"

          # Create bundle README
          cat > "$BUNDLE_DIR/README.md" << EOF
          # Model Asset Guard Bundle v$VERSION

          This bundle contains the verified components of the Model Asset Guard system.

          ## Contents

          - \`Spec/\` - Lean specification files with formal proofs
          - \`guardd/\` - Rust sidecar library for high-performance validation
          - \`bindings/\` - Python and Node.js bindings
          - \`lean-hash.txt\` - Lean kernel hash for verification

          ## Verification

          To verify this bundle:

          1. Check the Lean kernel hash:
             \`\`\`bash
             lake exe lean --version | head -1 | sha256sum
             \`\`\`
             Compare with the contents of \`lean-hash.txt\`

          2. Build and test the components:
             \`\`\`bash
             lake build
             lake exe tests
             cargo test --manifest-path src/rust/guardd/Cargo.toml
             \`\`\`

          ## License

          MIT License - see LICENSE file for details.
          EOF

          # Create bundle archive
          BUNDLE_NAME="model-asset-guard-$VERSION.zip"
          echo "Creating bundle archive: $BUNDLE_NAME"
          zip -r "$BUNDLE_NAME" "$BUNDLE_DIR"

          # Generate SHA-256 of bundle
          BUNDLE_SHA256=$(sha256sum "$BUNDLE_NAME" | cut -d' ' -f1)
          echo "Bundle SHA-256: $BUNDLE_SHA256"

          # Create release info
          cat > "release-info.txt" << EOF
          Model Asset Guard Bundle
          Version: $VERSION
          Date: $(date)
          Bundle: $BUNDLE_NAME
          SHA-256: $BUNDLE_SHA256
          Kernel Hash: $KERNEL_HASH
          EOF

          echo "Bundle created successfully!"
          echo "Bundle: $BUNDLE_NAME"
          echo "SHA-256: $BUNDLE_SHA256"

          # Cleanup
          rm -rf "$BUNDLE_DIR"

      - name: Upload bundle artifact
        uses: actions/upload-artifact@v4
        with:
          name: model-asset-guard-bundle-${{ github.sha }}
          path: |
            model-asset-guard-*.zip
            release-info.txt

      - name: Generate SBOM
        uses: anchore/sbom-action@v0
        with:
          path: .
          output-file: sbom.spdx.json
          format: spdx-json

      - name: Upload SBOM
        uses: actions/upload-artifact@v4
        with:
          name: sbom-${{ github.sha }}
          path: sbom.spdx.json

  publish-release:
    needs: create-bundle
    runs-on: ubuntu-latest
    if: startsWith(github.ref, 'refs/tags/')

    steps:
      - name: Checkout code
        uses: actions/checkout@v4

      - name: Download bundle artifact
        uses: actions/download-artifact@v4
        with:
          name: model-asset-guard-bundle-${{ github.sha }}
          path: ./bundles

      - name: Create GitHub Release
        uses: softprops/action-gh-release@v1
        with:
          files: |
            bundles/model-asset-guard-*.zip
            bundles/release-info.txt
          body: |
            ## Model Asset Guard v${{ github.ref_name }}

            This release includes:

            - ✅ Formal verification of all specifications
            - ✅ High-performance Rust sidecar library
            - ✅ Python and Node.js bindings
            - ✅ Comprehensive test suite
            - ✅ Bit-flip corpus validation
            - ✅ Quantization error bounds with 128-vector verification
            - ✅ Perfect hash tokenizer implementation

            ### Verification

            To verify this release:

            1. Check the Lean kernel hash in `lean-hash.txt`
            2. Run `lake build && lake exe tests`
            3. Run `cargo test --manifest-path guardd/Cargo.toml`

            ### Installation

            Extract the bundle and follow the README for integration instructions.

            ### SHA-256

            ```
            $(cat bundles/release-info.txt | grep SHA-256 | cut -d' ' -f2)
            ```
          draft: false
          prerelease: false
        env:
          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

  publish-to-registry:
    needs: create-bundle
    runs-on: ubuntu-latest
    if: startsWith(github.ref, 'refs/tags/')

    steps:
      - name: Checkout code
        uses: actions/checkout@v4

      - name: Download bundle artifact
        uses: actions/download-artifact@v4
        with:
          name: model-asset-guard-bundle-${{ github.sha }}
          path: ./bundles

      - name: Setup Python
        uses: actions/setup-python@v5
        with:
          python-version: "3.9"

      - name: Install Python dependencies
        run: |
          pip install build twine

      - name: Build Python package
        run: |
          cd bindings/python
          python -m build

      - name: Publish to PyPI
        if: github.ref == 'refs/tags/main'
        run: |
          cd bindings/python
          python -m twine upload dist/* --username __token__ --password ${{ secrets.PYPI_TOKEN }}
        env:
          TWINE_USERNAME: __token__
          TWINE_PASSWORD: ${{ secrets.PYPI_TOKEN }}

      - name: Publish to Test PyPI
        if: github.ref != 'refs/tags/main'
        run: |
          cd bindings/python
          python -m twine upload --repository testpypi dist/* --username __token__ --password ${{ secrets.TEST_PYPI_TOKEN }}
        env:
          TWINE_USERNAME: __token__
          TWINE_PASSWORD: ${{ secrets.TEST_PYPI_TOKEN }}