Skip to content
CI

docs: add comprehensive formal verification architecture documentation #48

Sign in to view logs

docs: add comprehensive formal verification architecture documentation

docs: add comprehensive formal verification architecture documentation #48

Workflow file for this run

.github/workflows/ci.yml at a4c4ab7
name: CI
on:
push:
branches: [ main ]
pull_request:
branches: [ main ]
env:
CARGO_TERM_COLOR: always
RUST_BACKTRACE: 1
jobs:
format:
name: Format
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- uses: dtolnay/rust-toolchain@stable
with:
components: rustfmt
- name: Check formatting
run: cargo fmt --all -- --check
clippy:
name: Clippy
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- uses: dtolnay/rust-toolchain@stable
with:
components: clippy
- uses: Swatinem/rust-cache@v2
- name: Install Z3
run: |
sudo apt-get update
sudo apt-get install -y z3
- name: Run clippy
run: cargo clippy --all-targets --all-features -- -D warnings
test:
name: Test
runs-on: ${{ matrix.os }}
strategy:
matrix:
os: [ubuntu-latest, macos-latest, windows-latest]
rust: [stable]
steps:
- uses: actions/checkout@v4
- uses: dtolnay/rust-toolchain@stable
- uses: Swatinem/rust-cache@v2
- name: Run tests
run: cargo test --all --verbose
build:
name: Build
runs-on: ${{ matrix.os }}
strategy:
matrix:
os: [ubuntu-latest, macos-latest, windows-latest]
steps:
- uses: actions/checkout@v4
- uses: dtolnay/rust-toolchain@stable
- uses: Swatinem/rust-cache@v2
- name: Build release
run: cargo build --release --verbose
- name: Upload artifacts
uses: actions/upload-artifact@v4
with:
name: loom-${{ matrix.os }}
path: |
target/release/loom
target/release/loom.exe
validate:
name: Validate WebAssembly Output
runs-on: ubuntu-latest
needs: build
steps:
- uses: actions/checkout@v4
- uses: dtolnay/rust-toolchain@stable
- uses: Swatinem/rust-cache@v2
- name: Install wasm-tools
run: cargo install wasm-tools
- name: Build loom
run: cargo build --release
- name: Optimize test fixtures
run: |
for fixture in tests/fixtures/*.wat; do
echo "Optimizing $fixture"
./target/release/loom optimize "$fixture" -o "/tmp/$(basename $fixture .wat).wasm"
wasm-tools validate "/tmp/$(basename $fixture .wat).wasm"
done
coverage:
name: Code Coverage
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- uses: dtolnay/rust-toolchain@stable
- uses: Swatinem/rust-cache@v2
- name: Install cargo-tarpaulin
run: cargo install cargo-tarpaulin
- name: Generate coverage
run: cargo tarpaulin --out xml --all-features
- name: Upload coverage to Codecov
uses: codecov/codecov-action@v4
with:
files: ./cobertura.xml
fail_ci_if_error: false
benchmark:
name: Benchmarks
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- uses: dtolnay/rust-toolchain@stable
- uses: Swatinem/rust-cache@v2
- name: Run benchmarks
run: cargo bench --no-fail-fast
verify:
name: Z3 Verification Build
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- uses: dtolnay/rust-toolchain@stable
- uses: Swatinem/rust-cache@v2
- name: Install Z3
run: |
sudo apt-get update
sudo apt-get install -y z3
- name: Build with verification feature
run: cargo build --release --features verification
- name: Test verification
run: |
./target/release/loom optimize tests/fixtures/test_input.wat \
-o /tmp/test.wasm --verify --stats
wasm-build:
name: WASM Build (wasm32-wasip2)
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- uses: dtolnay/rust-toolchain@stable
with:
targets: wasm32-wasip2
- uses: Swatinem/rust-cache@v2
- name: Build for wasm32-wasip2
run: cargo build --release --target wasm32-wasip2 --package loom-cli
- name: Upload WASM artifact
uses: actions/upload-artifact@v4
with:
name: loom-wasm
path: target/wasm32-wasip2/release/loom.wasm
self-optimization:
name: Self-Optimization Test
runs-on: ubuntu-latest
needs: [build, wasm-build]
steps:
- uses: actions/checkout@v4
- uses: dtolnay/rust-toolchain@stable
- uses: Swatinem/rust-cache@v2
- name: Install wasm-tools
run: cargo install wasm-tools
- name: Download LOOM binary
uses: actions/download-artifact@v4
with:
name: loom-ubuntu-latest
path: ./loom-bin
- name: Download LOOM WASM
uses: actions/download-artifact@v4
with:
name: loom-wasm
path: ./loom-wasm
- name: Make binary executable
run: chmod +x ./loom-bin/loom
- name: Test self-optimization
run: |
echo "Testing LOOM self-optimization (dogfooding)..."
INPUT="./loom-wasm/loom.wasm"
OUTPUT="/tmp/loom-optimized.wasm"
# Verify input is valid
wasm-tools validate "$INPUT" || { echo "Input validation failed"; exit 1; }
# Optimize LOOM with itself
./loom-bin/loom optimize "$INPUT" -o "$OUTPUT" --stats || { echo "Optimization failed"; exit 1; }
# Verify output is valid
wasm-tools validate "$OUTPUT" || { echo "Output validation failed"; exit 1; }
# Calculate size reduction
INPUT_SIZE=$(stat -f%z "$INPUT" 2>/dev/null || stat -c%s "$INPUT")
OUTPUT_SIZE=$(stat -f%z "$OUTPUT" 2>/dev/null || stat -c%s "$OUTPUT")
REDUCTION=$((100 * (INPUT_SIZE - OUTPUT_SIZE) / INPUT_SIZE))
echo "✅ Self-optimization successful!"
echo " Input: $INPUT_SIZE bytes"
echo " Output: $OUTPUT_SIZE bytes"
echo " Reduction: $REDUCTION%"