Linear type system for WebAssembly memory safety

.github/workflows/ci.yml

@@ -0,0 +1,161 @@
+# SPDX-License-Identifier: EUPL-1.2
+# SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell
+
+name: CI
+
+on:
+  push:
+    branches: [main, develop]
+  pull_request:
+    branches: [main]
+
+env:
+  CARGO_TERM_COLOR: always
+  RUSTFLAGS: "-D warnings"
+
+jobs:
+  # ==========================================================================
+  # Rust Checks
+  # ==========================================================================
+
+  lint:
+    name: Lint
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Install Rust
+        uses: dtolnay/rust-action@stable
+        with:
+          components: rustfmt, clippy
+
+      - name: Cache cargo
+        uses: Swatinem/rust-cache@v2
+
+      - name: Check formatting
+        run: cargo fmt --all -- --check
+
+      - name: Clippy
+        run: cargo clippy --all-targets --all-features -- -D warnings
+
+  build:
+    name: Build
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        target:
+          - x86_64-unknown-linux-gnu
+          - wasm32-unknown-unknown
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Install Rust
+        uses: dtolnay/rust-action@stable
+        with:
+          targets: ${{ matrix.target }}
+
+      - name: Cache cargo
+        uses: Swatinem/rust-cache@v2
+
+      - name: Build
+        run: cargo build --release --target ${{ matrix.target }}
+
+      - name: Upload artifacts
+        if: matrix.target == 'wasm32-unknown-unknown'
+        uses: actions/upload-artifact@v4
+        with:
+          name: wasm-artifacts
+          path: target/wasm32-unknown-unknown/release/*.wasm
+
+  test:
+    name: Test
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Install Rust
+        uses: dtolnay/rust-action@stable
+
+      - name: Cache cargo
+        uses: Swatinem/rust-cache@v2
+
+      - name: Run tests
+        run: cargo test --all-features --verbose
+
+  # ==========================================================================
+  # Coq Proofs
+  # ==========================================================================
+
+  coq:
+    name: Coq Proofs
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Install Coq
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y coq
+
+      - name: Cache Coq
+        uses: actions/cache@v4
+        with:
+          path: |
+            formal/*.vo
+            formal/*.glob
+          key: coq-${{ hashFiles('formal/*.v') }}
+
+      - name: Build proofs
+        run: |
+          cd formal
+          make depend
+          make -j$(nproc)
+
+      - name: Check for Admitted
+        run: |
+          cd formal
+          count=$(grep -r "Admitted\." *.v | wc -l)
+          echo "Found $count Admitted proofs"
+          # Allow some admitted proofs during development
+          if [ "$count" -gt 10 ]; then
+            echo "Warning: Too many Admitted proofs"
+          fi
+
+  # ==========================================================================
+  # Documentation
+  # ==========================================================================
+
+  docs:
+    name: Documentation
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Install Rust
+        uses: dtolnay/rust-action@stable
+
+      - name: Cache cargo
+        uses: Swatinem/rust-cache@v2
+
+      - name: Build docs
+        run: cargo doc --no-deps --all-features
+
+      - name: Upload docs
+        uses: actions/upload-artifact@v4
+        with:
+          name: rustdoc
+          path: target/doc
+
+  # ==========================================================================
+  # REUSE Compliance
+  # ==========================================================================
+
+  reuse:
+    name: REUSE Compliance
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: REUSE Compliance Check
+        uses: fsfe/reuse-action@v4
+        continue-on-error: true  # Advisory during development

CONTRIBUTING.adoc

@@ -0,0 +1,112 @@
+// SPDX-License-Identifier: EUPL-1.2
+// SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell
+
+= Contributing to Ephapax
+
+Thank you for your interest in contributing to Ephapax!
+
+== Getting Started
+
+=== Prerequisites
+
+* Rust 1.83+
+* Coq 8.18+ (for formal proofs)
+* wasm32-unknown-unknown target
+
+=== Development Setup
+
+[source,bash]
+----
+# Clone the repository
+git clone https://github.com/hyperpolymath/ephapax.git
+cd ephapax
+
+# Install WASM target
+rustup target add wasm32-unknown-unknown
+
+# Build
+cargo build
+
+# Run tests
+cargo test --all-features
+
+# Build Coq proofs
+cd formal && make
+----
+
+== Code Style
+
+=== Rust
+
+* Follow standard Rust conventions
+* Use `cargo fmt` before committing
+* Run `cargo clippy` and address warnings
+* Add tests for new functionality
+
+=== Coq
+
+* Document lemmas and theorems
+* Use meaningful names
+* Minimize `Admitted` proofs
+
+== Pull Request Process
+
+1. Fork the repository
+2. Create a feature branch: `git checkout -b feature/my-feature`
+3. Make your changes
+4. Run tests: `cargo test && cd formal && make`
+5. Commit with clear messages
+6. Push and open a PR
+
+== Commit Messages
+
+Use conventional commits:
+
+* `feat:` New feature
+* `fix:` Bug fix
+* `docs:` Documentation
+* `refactor:` Code refactoring
+* `test:` Adding tests
+* `chore:` Maintenance
+
+Example:
+
+----
+feat(typing): add region escape checking
+
+Implements the T-Region typing rule to prevent
+region-scoped types from escaping their region.
+
+Closes #42
+----
+
+== Areas for Contribution
+
+=== High Priority
+
+* Lexer implementation
+* Parser implementation
+* Type checker completion
+* WASM codegen improvements
+
+=== Medium Priority
+
+* REPL implementation
+* Standard library
+* Documentation improvements
+* Error message improvements
+
+=== Research
+
+* Typestate extensions
+* Fractional permissions
+* Concurrency support
+
+== Questions?
+
+* Open an issue for questions
+* Check existing issues for similar topics
+
+== Licence
+
+Contributions are licensed under EUPL-1.2.