feat: add comprehensive test suite (339 tests), property/mutation/compat tests

- property_tests.rs: 41 property-based tests (all 7 number systems)
- harvard_boundary_tests.rs: 35 security boundary tests (code injection grammar rejection)
- mutation_killers.rs: mutation test suite
- contract_tests.rs + compatibility_tests.rs: contract and compat tests
- coverage.yml + proof-regression.yml: new CI workflows
- Grammar, purity checker, reversible semantics improvements
- Fixed empty_file.jtv classification (valid, not invalid)

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/coverage.yml

@@ -0,0 +1,71 @@
+# SPDX-License-Identifier: PMPL-1.0-or-later
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# coverage.yml — Code coverage reporting via cargo-tarpaulin.
+# Generates coverage report and uploads to Codecov.
+name: Coverage
+
+on:
+  pull_request:
+    branches: ['**']
+  push:
+    branches: [main]
+
+permissions:
+  contents: read
+
+jobs:
+  coverage:
+    name: Code coverage
+    runs-on: ubuntu-latest
+    if: hashFiles('Cargo.toml') != ''
+
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
+
+      - name: Install Rust toolchain
+        uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7 # stable
+
+      - name: Cache cargo registry and build
+        uses: Swatinem/rust-cache@779680da715d629ac1d338a641029a2f4372abb5 # v2
+
+      - name: Install cargo-tarpaulin
+        run: cargo install cargo-tarpaulin
+
+      - name: Generate coverage report
+        run: |
+          cargo tarpaulin \
+            -p jtv-core \
+            --out xml \
+            --out html \
+            --output-dir coverage/ \
+            --skip-clean \
+            --timeout 120
+
+      - name: Upload to Codecov
+        uses: codecov/codecov-action@671740ac38dd9b0130fbe1cec585b89eea48d3de # v5
+        with:
+          files: coverage/cobertura.xml
+          fail_ci_if_error: false
+
+      - name: Write summary
+        if: always()
+        run: |
+          echo "## Code Coverage Report" >> "$GITHUB_STEP_SUMMARY"
+          echo "" >> "$GITHUB_STEP_SUMMARY"
+          if [ -f coverage/cobertura.xml ]; then
+            LINE_RATE=$(grep -oP 'line-rate="\K[^"]+' coverage/cobertura.xml | head -1)
+            PERCENT=$(echo "$LINE_RATE * 100" | bc -l 2>/dev/null | head -c 5 || echo "$LINE_RATE")
+            echo "Line coverage: **${PERCENT}%**" >> "$GITHUB_STEP_SUMMARY"
+          else
+            echo "Coverage report not generated." >> "$GITHUB_STEP_SUMMARY"
+          fi
+
+      - name: Upload HTML report as artifact
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: coverage-report
+          path: coverage/
+          retention-days: 30

.github/workflows/proof-regression.yml

@@ -0,0 +1,94 @@
+# SPDX-License-Identifier: PMPL-1.0-or-later
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# proof-regression.yml — Verify that formal proofs still compile after code changes.
+# Covers: Lean 4 mechanized proofs (jtv_proofs/) and Idris2 ABI types (src/abi/).
+# Taxonomy category: Proof Regression (PRF)
+name: Proof Regression
+
+on:
+  pull_request:
+    branches: ['**']
+    paths:
+      - 'jtv_proofs/**'
+      - 'src/abi/**'
+      - 'crates/jtv-core/src/ast.rs'
+      - 'crates/jtv-core/src/number.rs'
+      - 'crates/jtv-core/src/reversible.rs'
+      - 'crates/jtv-core/src/grammar.pest'
+  push:
+    branches: [main]
+    paths:
+      - 'jtv_proofs/**'
+      - 'src/abi/**'
+      - 'crates/jtv-core/src/ast.rs'
+      - 'crates/jtv-core/src/number.rs'
+      - 'crates/jtv-core/src/reversible.rs'
+      - 'crates/jtv-core/src/grammar.pest'
+  # Also run weekly to catch upstream Lean/Idris2 breakage
+  schedule:
+    - cron: '0 6 * * 1'
+
+permissions:
+  contents: read
+
+jobs:
+  lean4-proofs:
+    name: Lean 4 proof verification
+    runs-on: ubuntu-latest
+    if: hashFiles('jtv_proofs/lakefile.lean') != ''
+
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
+
+      - name: Install elan (Lean toolchain manager)
+        run: |
+          curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+
+      - name: Cache Lean build
+        uses: actions/cache@v4
+        with:
+          path: |
+            jtv_proofs/.lake
+            jtv_proofs/build
+          key: lean4-${{ hashFiles('jtv_proofs/lakefile.lean', 'jtv_proofs/lean-toolchain') }}
+          restore-keys: lean4-
+
+      - name: Build Lean proofs
+        working-directory: jtv_proofs
+        run: |
+          lake build
+          echo "## Lean 4 Proof Verification" >> "$GITHUB_STEP_SUMMARY"
+          echo "" >> "$GITHUB_STEP_SUMMARY"
+          echo "All proofs compiled successfully." >> "$GITHUB_STEP_SUMMARY"
+
+  idris2-abi:
+    name: Idris2 ABI type verification
+    runs-on: ubuntu-latest
+    if: hashFiles('src/abi/Types.idr') != ''
+
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
+
+      - name: Install Idris2
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y idris2 || {
+            # Fallback: install from pack
+            curl -sSf https://raw.githubusercontent.com/stefan-hoeck/idris2-pack/main/install.bash | bash
+            echo "$HOME/.pack/bin" >> "$GITHUB_PATH"
+          }
+
+      - name: Check Idris2 ABI types
+        run: |
+          cd src/abi
+          idris2 --check Types.idr || {
+            echo "::error::Idris2 ABI type definitions failed to compile"
+            exit 1
+          }
+          echo "## Idris2 ABI Verification" >> "$GITHUB_STEP_SUMMARY"
+          echo "" >> "$GITHUB_STEP_SUMMARY"
+          echo "ABI type definitions verified successfully." >> "$GITHUB_STEP_SUMMARY"

.github/workflows/rust-ci.yml

@@ -2,6 +2,7 @@
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # rust-ci.yml — Cargo build, test, clippy, and fmt for Rust projects.
+# Cross-platform matrix: Linux, macOS, Windows.
 # Only runs if Cargo.toml exists in the repo root.
 name: Rust CI
 
@@ -16,9 +17,13 @@ permissions:
 
 jobs:
   check:
-    name: Cargo check + clippy + fmt
-    runs-on: ubuntu-latest
+    name: Check (${{ matrix.os }})
+    runs-on: ${{ matrix.os }}
     if: hashFiles('Cargo.toml') != ''
+    strategy:
+      fail-fast: false
+      matrix:
+        os: [ubuntu-latest, macos-latest, windows-latest]
 
     steps:
       - name: Checkout repository
@@ -42,10 +47,14 @@ jobs:
         run: cargo clippy --all-targets -- -D warnings
 
   test:
-    name: Cargo test
-    runs-on: ubuntu-latest
+    name: Test (${{ matrix.os }})
+    runs-on: ${{ matrix.os }}
     needs: check
     if: hashFiles('Cargo.toml') != ''
+    strategy:
+      fail-fast: false
+      matrix:
+        os: [ubuntu-latest, macos-latest, windows-latest]
 
     steps:
       - name: Checkout repository
@@ -63,7 +72,7 @@ jobs:
       - name: Write summary
         if: always()
         run: |
-          echo "## Rust CI Results" >> "$GITHUB_STEP_SUMMARY"
+          echo "## Rust CI Results (${{ matrix.os }})" >> "$GITHUB_STEP_SUMMARY"
           echo "" >> "$GITHUB_STEP_SUMMARY"
           echo "- **cargo check**: passed" >> "$GITHUB_STEP_SUMMARY"
           echo "- **cargo test**: completed" >> "$GITHUB_STEP_SUMMARY"

Cargo.toml

@@ -50,6 +50,7 @@ dirs = "5.0"
 # Testing
 criterion = "0.5"
 insta = "1"
+proptest = "1.4"
 
 # Async runtime
 tokio = "1.0"

Justfile

@@ -214,19 +214,56 @@ build-pwa: build-wasm
     @echo "✅ PWA files in web/"
     @echo "📝 Ready to deploy!"
 
+# Smoke test: fast sanity check (<30 seconds). Taxonomy: SMK
+smoke:
+    @echo "Running smoke test..."
+    @echo "  [1/4] Cargo check (jtv-core)..."
+    @cargo check --quiet -p jtv-core 2>&1
+    @echo "  [OK] Build compiles"
+    @echo "  [2/4] Parse conformance file..."
+    @cargo run --quiet --bin jtv parse conformance/valid/data_expressions.jtv 2>&1 > /dev/null
+    @echo "  [OK] Parser works"
+    @echo "  [3/4] Run unit tests (quick)..."
+    @cargo test --quiet -p jtv-core --lib 2>&1 > /dev/null
+    @echo "  [OK] Unit tests pass"
+    @echo "  [4/4] Clippy (jtv-core, no warnings)..."
+    @cargo clippy --quiet -p jtv-core -- -D warnings 2>&1 > /dev/null
+    @echo "  [OK] No clippy warnings"
+    @echo "Smoke test passed."
+
 # Run panic-attacker pre-commit scan
 assail:
     @command -v panic-attack >/dev/null 2>&1 && panic-attack assail . || echo "panic-attack not found — install from https://github.com/hyperpolymath/panic-attacker"
 
-# Self-diagnostic — checks dependencies, permissions, paths
+# Self-diagnostic — checks dependencies, permissions, paths, proofs. Taxonomy: REF
 doctor:
     @echo "Running diagnostics for julia-the-viper..."
-    @echo "Checking required tools..."
-    @command -v just >/dev/null 2>&1 && echo "  [OK] just" || echo "  [FAIL] just not found"
-    @command -v git >/dev/null 2>&1 && echo "  [OK] git" || echo "  [FAIL] git not found"
-    @echo "Checking for hardcoded paths..."
-    @grep -rn '$HOME\|$ECLIPSE_DIR' --include='*.rs' --include='*.ex' --include='*.res' --include='*.gleam' --include='*.sh' . 2>/dev/null | head -5 || echo "  [OK] No hardcoded paths"
-    @echo "Diagnostics complete."
+    @FAIL=0; \
+    echo "=== Required Tools ==="; \
+    command -v just >/dev/null 2>&1 && echo "  [OK] just" || { echo "  [FAIL] just not found"; FAIL=1; }; \
+    command -v cargo >/dev/null 2>&1 && echo "  [OK] cargo ($(cargo --version 2>/dev/null | head -c 20))" || { echo "  [FAIL] cargo not found"; FAIL=1; }; \
+    command -v git >/dev/null 2>&1 && echo "  [OK] git" || { echo "  [FAIL] git not found"; FAIL=1; }; \
+    echo "=== Project Structure ==="; \
+    test -f Cargo.toml && echo "  [OK] Cargo.toml" || { echo "  [FAIL] Cargo.toml missing"; FAIL=1; }; \
+    test -f Justfile && echo "  [OK] Justfile" || { echo "  [FAIL] Justfile missing"; FAIL=1; }; \
+    test -f LICENSE && echo "  [OK] LICENSE" || { echo "  [FAIL] LICENSE missing"; FAIL=1; }; \
+    test -d crates/jtv-core/src && echo "  [OK] crates/jtv-core/src/" || { echo "  [FAIL] core crate missing"; FAIL=1; }; \
+    test -f crates/jtv-core/src/grammar.pest && echo "  [OK] grammar.pest" || { echo "  [FAIL] grammar.pest missing"; FAIL=1; }; \
+    echo "=== Formal Proofs ==="; \
+    test -d jtv_proofs && echo "  [OK] jtv_proofs/ (Lean 4)" || echo "  [WARN] jtv_proofs/ missing"; \
+    test -f src/abi/Types.idr && echo "  [OK] src/abi/Types.idr (Idris2)" || echo "  [WARN] src/abi/Types.idr missing"; \
+    echo "=== Conformance Suite ==="; \
+    VALID=$(ls conformance/valid/*.jtv 2>/dev/null | wc -l); \
+    INVALID=$(ls conformance/invalid/*.jtv 2>/dev/null | wc -l); \
+    echo "  [INFO] $VALID valid programs, $INVALID invalid programs"; \
+    echo "=== Security Checks ==="; \
+    grep -rn 'believe_me\|assert_total\|sorry\|Admitted\|unsafeCoerce' --include='*.rs' --include='*.idr' --include='*.lean' . 2>/dev/null | grep -v target/ | head -5 && { echo "  [WARN] Dangerous patterns found"; } || echo "  [OK] No dangerous patterns"; \
+    echo "=== Hardcoded Paths ==="; \
+    grep -rn '\$HOME\|\$ECLIPSE_DIR\|/home/' --include='*.rs' --include='*.ex' --include='*.sh' . 2>/dev/null | grep -v target/ | head -5 && echo "  [WARN] Hardcoded paths found" || echo "  [OK] No hardcoded paths"; \
+    echo "=== Test Count ==="; \
+    TESTS=$(grep -r '#\[test\]' crates/ --include='*.rs' 2>/dev/null | grep -v target/ | wc -l); \
+    echo "  [INFO] $TESTS tests found"; \
+    if [ $FAIL -gt 0 ]; then echo "DIAGNOSTICS: FAILED ($FAIL issues)"; exit 1; else echo "DIAGNOSTICS: PASSED"; fi
 
 # Auto-repair common issues
 heal: