Skip to content

Commit 9350b2b

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
feat: Initial Ephapax language implementation (#1)
Ephapax is a linear type system for safe memory management targeting WebAssembly. This commit includes: Core Implementation: - ephapax-syntax: AST definitions with linear type annotations - ephapax-typing: Linear type checker with region support - ephapax-wasm: WASM code generator with bump allocation - ephapax-runtime: no_std WASM runtime with region management Formal Semantics (Coq): - Syntax.v: Core type and expression definitions - Typing.v: Linear typing rules with context tracking - Semantics.v: Operational semantics and safety theorems Documentation: - Language specification (spec/SPEC.md) - Comprehensive wiki documentation - ROADMAP.md with detailed development plan - CONTRIBUTING.adoc guide Infrastructure: - Cargo workspace with 4 crates - CI/CD workflow for Rust and Coq - EUPL-1.2 license Key features: - Linear types prevent use-after-free and memory leaks - Region-based memory management for bulk deallocation - Second-class borrows for temporary access - Formal proofs in Coq for type safety Co-authored-by: Claude <noreply@anthropic.com>
1 parent 9a30ad4 commit 9350b2b

33 files changed

Lines changed: 6780 additions & 76 deletions

File tree

‎.github/workflows/ci.yml‎

Lines changed: 161 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,161 @@
1+
# SPDX-License-Identifier: EUPL-1.2
2+
# SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell
3+
4+
name: CI
5+
6+
on:
7+
push:
8+
branches: [main, develop]
9+
pull_request:
10+
branches: [main]
11+
12+
env:
13+
CARGO_TERM_COLOR: always
14+
RUSTFLAGS: "-D warnings"
15+
16+
jobs:
17+
# ==========================================================================
18+
# Rust Checks
19+
# ==========================================================================
20+
21+
lint:
22+
name: Lint
23+
runs-on: ubuntu-latest
24+
steps:
25+
- uses: actions/checkout@v4
26+
27+
- name: Install Rust
28+
uses: dtolnay/rust-action@stable
29+
with:
30+
components: rustfmt, clippy
31+
32+
- name: Cache cargo
33+
uses: Swatinem/rust-cache@v2
34+
35+
- name: Check formatting
36+
run: cargo fmt --all -- --check
37+
38+
- name: Clippy
39+
run: cargo clippy --all-targets --all-features -- -D warnings
40+
41+
build:
42+
name: Build
43+
runs-on: ubuntu-latest
44+
strategy:
45+
matrix:
46+
target:
47+
- x86_64-unknown-linux-gnu
48+
- wasm32-unknown-unknown
49+
steps:
50+
- uses: actions/checkout@v4
51+
52+
- name: Install Rust
53+
uses: dtolnay/rust-action@stable
54+
with:
55+
targets: ${{ matrix.target }}
56+
57+
- name: Cache cargo
58+
uses: Swatinem/rust-cache@v2
59+
60+
- name: Build
61+
run: cargo build --release --target ${{ matrix.target }}
62+
63+
- name: Upload artifacts
64+
if: matrix.target == 'wasm32-unknown-unknown'
65+
uses: actions/upload-artifact@v4
66+
with:
67+
name: wasm-artifacts
68+
path: target/wasm32-unknown-unknown/release/*.wasm
69+
70+
test:
71+
name: Test
72+
runs-on: ubuntu-latest
73+
steps:
74+
- uses: actions/checkout@v4
75+
76+
- name: Install Rust
77+
uses: dtolnay/rust-action@stable
78+
79+
- name: Cache cargo
80+
uses: Swatinem/rust-cache@v2
81+
82+
- name: Run tests
83+
run: cargo test --all-features --verbose
84+
85+
# ==========================================================================
86+
# Coq Proofs
87+
# ==========================================================================
88+
89+
coq:
90+
name: Coq Proofs
91+
runs-on: ubuntu-latest
92+
steps:
93+
- uses: actions/checkout@v4
94+
95+
- name: Install Coq
96+
run: |
97+
sudo apt-get update
98+
sudo apt-get install -y coq
99+
100+
- name: Cache Coq
101+
uses: actions/cache@v4
102+
with:
103+
path: |
104+
formal/*.vo
105+
formal/*.glob
106+
key: coq-${{ hashFiles('formal/*.v') }}
107+
108+
- name: Build proofs
109+
run: |
110+
cd formal
111+
make depend
112+
make -j$(nproc)
113+
114+
- name: Check for Admitted
115+
run: |
116+
cd formal
117+
count=$(grep -r "Admitted\." *.v | wc -l)
118+
echo "Found $count Admitted proofs"
119+
# Allow some admitted proofs during development
120+
if [ "$count" -gt 10 ]; then
121+
echo "Warning: Too many Admitted proofs"
122+
fi
123+
124+
# ==========================================================================
125+
# Documentation
126+
# ==========================================================================
127+
128+
docs:
129+
name: Documentation
130+
runs-on: ubuntu-latest
131+
steps:
132+
- uses: actions/checkout@v4
133+
134+
- name: Install Rust
135+
uses: dtolnay/rust-action@stable
136+
137+
- name: Cache cargo
138+
uses: Swatinem/rust-cache@v2
139+
140+
- name: Build docs
141+
run: cargo doc --no-deps --all-features
142+
143+
- name: Upload docs
144+
uses: actions/upload-artifact@v4
145+
with:
146+
name: rustdoc
147+
path: target/doc
148+
149+
# ==========================================================================
150+
# REUSE Compliance
151+
# ==========================================================================
152+
153+
reuse:
154+
name: REUSE Compliance
155+
runs-on: ubuntu-latest
156+
steps:
157+
- uses: actions/checkout@v4
158+
159+
- name: REUSE Compliance Check
160+
uses: fsfe/reuse-action@v4
161+
continue-on-error: true # Advisory during development

‎CONTRIBUTING.adoc‎

Lines changed: 112 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,112 @@
1+
// SPDX-License-Identifier: EUPL-1.2
2+
// SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell
3+
4+
= Contributing to Ephapax
5+
6+
Thank you for your interest in contributing to Ephapax!
7+
8+
== Getting Started
9+
10+
=== Prerequisites
11+
12+
* Rust 1.83+
13+
* Coq 8.18+ (for formal proofs)
14+
* wasm32-unknown-unknown target
15+
16+
=== Development Setup
17+
18+
[source,bash]
19+
----
20+
# Clone the repository
21+
git clone https://github.com/hyperpolymath/ephapax.git
22+
cd ephapax
23+
24+
# Install WASM target
25+
rustup target add wasm32-unknown-unknown
26+
27+
# Build
28+
cargo build
29+
30+
# Run tests
31+
cargo test --all-features
32+
33+
# Build Coq proofs
34+
cd formal && make
35+
----
36+
37+
== Code Style
38+
39+
=== Rust
40+
41+
* Follow standard Rust conventions
42+
* Use `cargo fmt` before committing
43+
* Run `cargo clippy` and address warnings
44+
* Add tests for new functionality
45+
46+
=== Coq
47+
48+
* Document lemmas and theorems
49+
* Use meaningful names
50+
* Minimize `Admitted` proofs
51+
52+
== Pull Request Process
53+
54+
1. Fork the repository
55+
2. Create a feature branch: `git checkout -b feature/my-feature`
56+
3. Make your changes
57+
4. Run tests: `cargo test && cd formal && make`
58+
5. Commit with clear messages
59+
6. Push and open a PR
60+
61+
== Commit Messages
62+
63+
Use conventional commits:
64+
65+
* `feat:` New feature
66+
* `fix:` Bug fix
67+
* `docs:` Documentation
68+
* `refactor:` Code refactoring
69+
* `test:` Adding tests
70+
* `chore:` Maintenance
71+
72+
Example:
73+
74+
----
75+
feat(typing): add region escape checking
76+
77+
Implements the T-Region typing rule to prevent
78+
region-scoped types from escaping their region.
79+
80+
Closes #42
81+
----
82+
83+
== Areas for Contribution
84+
85+
=== High Priority
86+
87+
* Lexer implementation
88+
* Parser implementation
89+
* Type checker completion
90+
* WASM codegen improvements
91+
92+
=== Medium Priority
93+
94+
* REPL implementation
95+
* Standard library
96+
* Documentation improvements
97+
* Error message improvements
98+
99+
=== Research
100+
101+
* Typestate extensions
102+
* Fractional permissions
103+
* Concurrency support
104+
105+
== Questions?
106+
107+
* Open an issue for questions
108+
* Check existing issues for similar topics
109+
110+
== Licence
111+
112+
Contributions are licensed under EUPL-1.2.

0 commit comments

Comments
 (0)