Skip to content

Commit 244cd2f

Browse files
author
Arnaud Riess
committed
Refactor docs structure for improved readability and maintainability
1 parent 2ef8997 commit 244cd2f

8 files changed

Lines changed: 1157 additions & 2111 deletions

File tree

CHANGELOG.md

Lines changed: 1 addition & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -68,25 +68,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
6868

6969
Many tests are missing!
7070

71-
**Current Phase**: Milestone 3 complete (Import/Export System)
72-
73-
**Completed**:
74-
- ✅ Phase 0: Workspace scaffold
75-
- ✅ Phase 1: Runtime core (herkos-runtime)
76-
- ✅ Milestone 1: Arithmetic and memory operations
77-
- ✅ Milestone 2: Control flow (if/block/loop/br)
78-
- ✅ Milestone 3: Import/Export system
79-
80-
**In Progress**:
81-
- 🔄 Pre-open-source code review and cleanup
82-
83-
**Planned**:
84-
- ⏳ Backend selection (verified/hybrid modes)
85-
- ⏳ Local variable tracking
86-
- ⏳ Multi-value blocks
87-
- ⏳ WASI, optimization, documentation
88-
89-
See [PLAN.md](PLAN.md) for the complete roadmap.
71+
See [docs/FUTURE.md](docs/FUTURE.md) for planned features.
9072

9173
## Version History
9274

CLAUDE.md

Lines changed: 86 additions & 134 deletions
Original file line numberDiff line numberDiff line change
@@ -6,15 +6,53 @@
66

77
The pipeline: **WebAssembly → Rust source → Safe binary**
88

9-
See the `docs/` directory for the full draft specification.
9+
## Documentation
10+
11+
| Document | Purpose |
12+
|----------|---------|
13+
| `docs/REQUIREMENTS.md` | What the system must do — formal requirements with REQ_* IDs |
14+
| `docs/SPECIFICATION.md` | How it works — module representation, architecture, transpilation rules, integration, performance. Also includes getting started guide. |
15+
| `docs/FUTURE.md` | Planned but unimplemented features — verified/hybrid backends, temporal isolation, contract-based verification |
1016

1117
## Repository structure
1218

1319
The project is a Rust workspace with three crates:
1420

15-
- `crates/herkos/` — CLI transpiler: parses `.wasm` binaries and emits Rust source code
16-
- `crates/herkos-runtime/` — Runtime library shipped with transpiled output (`IsolatedMemory`, capability types, Wasm operations)
17-
- `crates/herkos-tests/` — Integration test library
21+
| Crate | Purpose | `no_std` |
22+
|-------|---------|----------|
23+
| `crates/herkos/` | CLI transpiler: parses `.wasm` binaries, emits Rust source code | No (`std`) |
24+
| `crates/herkos-runtime/` | Runtime library shipped with transpiled output | **Yes** |
25+
| `crates/herkos-tests/` | Integration tests + benchmarks: WAT/C/Rust → .wasm → transpile → test | No (`std`) |
26+
27+
### Transpiler pipeline (`crates/herkos/src/`)
28+
29+
```
30+
.wasm → parser/ → ir/builder/ → optimizer/ → backend/safe.rs → codegen/ → rustfmt
31+
(wasmparser) (SSA IR) (dead blocks) (SafeBackend) (Rust source)
32+
```
33+
34+
Key modules:
35+
- `parser/` — Wasm binary parsing via `wasmparser` crate
36+
- `ir/` — SSA-form intermediate representation (`ModuleInfo`, `IrFunction`, `IrBlock`, `IrInstr`)
37+
- `ir/builder/` — Wasm → IR translation (core.rs, translate.rs, assembly.rs, analysis.rs)
38+
- `optimizer/` — IR optimization passes (currently: dead block elimination)
39+
- `backend/` — Backend trait + `SafeBackend` (bounds-checked, no unsafe)
40+
- `codegen/` — IR → Rust source (module.rs, function.rs, instruction.rs, traits.rs, export.rs, constructor.rs)
41+
42+
### Runtime (`crates/herkos-runtime/src/`)
43+
44+
- `memory.rs``IsolatedMemory<MAX_PAGES>`: load/store methods, memory.grow/size, Kani proofs
45+
- `table.rs``Table<MAX_SIZE>`, `FuncRef`: indirect call dispatch
46+
- `module.rs``Module<G, MAX_PAGES, TABLE_SIZE>`, `LibraryModule<G, TABLE_SIZE>`
47+
- `ops.rs` — Wasm arithmetic operations with trap handling (div, rem, trunc)
48+
- `lib.rs``WasmTrap`, `WasmResult<T>`, `ConstructionError`, `PAGE_SIZE`
49+
50+
### Tests (`crates/herkos-tests/`)
51+
52+
- `build.rs` — Compiles WAT/C/Rust sources to `.wasm`, invokes transpiler, writes to `OUT_DIR`
53+
- `tests/` — Integration tests: arithmetic, memory, control flow, imports/exports, E2E (C and Rust)
54+
- `benches/` — Criterion benchmarks (Fibonacci)
55+
- `data/rust/` — Pre-generated Rust test modules
1856

1957
## Build and test
2058

@@ -23,6 +61,7 @@ cargo build # build all crates
2361
cargo test # run all tests
2462
cargo clippy --all-targets # lint (CI enforced)
2563
cargo fmt --check # format check (CI enforced)
64+
cargo bench -p herkos-tests # benchmarks
2665
```
2766

2867
Run a single crate's tests:
@@ -32,12 +71,7 @@ cargo test -p herkos-runtime
3271
cargo test -p herkos-tests
3372
```
3473

35-
Build documentation (sphinx):
36-
```bash
37-
cd docs && uv run make clean && uv run make html # build Sphinx documentation
38-
```
39-
40-
CLI usage (once built):
74+
CLI usage:
4175
```bash
4276
cargo run -p herkos -- input.wasm --output output.rs
4377
```
@@ -46,160 +80,78 @@ cargo run -p herkos -- input.wasm --output output.rs
4680

4781
### Memory model
4882

49-
Wasm linear memory is represented as a page-level const generic:
50-
51-
```rust
52-
struct IsolatedMemory<const MAX_PAGES: usize> {
53-
pages: [[u8; PAGE_SIZE]; MAX_PAGES], // Fully allocated at compile time, contiguous
54-
active_pages: usize, // Current live size (starts at initial_pages)
55-
}
56-
```
83+
Wasm linear memory is `IsolatedMemory<const MAX_PAGES: usize>` — a 2D array `[[u8; PAGE_SIZE]; MAX_PAGES]` with `active_pages` tracking. Fully allocated at compile time, no heap. See `crates/herkos-runtime/src/memory.rs` and SPECIFICATION.md §2.1.
5784

58-
**Design decisions**:
59-
- **`MAX_PAGES` const generic**: Derived from the Wasm module's declared maximum. Prevents any heap allocation (`no_std` compatible). Enables monomorphization for zero-cost dispatch.
60-
- **`active_pages` tracking**: Starts at the module's initial page count. Incremented by `memory.grow`. Accesses beyond `active_pages * PAGE_SIZE` trap.
61-
- **2D layout** `[[u8; PAGE_SIZE]; MAX_PAGES]`: Avoids `generic_const_exprs` (unstable Rust feature). Contiguous in memory. `as_flattened()` provides flat `&[u8]` views.
85+
### Module types
6286

63-
**Memory access API**:
64-
- **Safe**: `load_i32(offset) -> WasmResult<i32>` (bounds-checked)
65-
- **Verified**: `unsafe load_i32_unchecked(offset) -> i32` (proof-justified)
87+
Two kinds:
88+
1. **`Module<G, MAX_PAGES, TABLE_SIZE>`** — Owns memory (process-like)
89+
2. **`LibraryModule<G, TABLE_SIZE>`** — Borrows caller's memory (library-like)
6690

67-
No `MemoryView` wrappers — the API is flat and fast. See SPECIFICATION.md §3 for complete details.
91+
Each has a **Globals struct** `G` (one typed field per mutable Wasm global) and a **Table** for indirect calls. See `crates/herkos-runtime/src/module.rs` and SPECIFICATION.md §2.2.
6892

69-
### Module representation
70-
71-
Two kinds of modules:
93+
### Capability-based security via traits
7294

73-
1. **`Module<G, MAX_PAGES, TABLE_SIZE>`** — Owns its own memory (like a process)
74-
2. **`LibraryModule<G, TABLE_SIZE>`** — Borrows memory from caller (like a shared library)
95+
- **Imports** → trait bounds on generic host parameter `H`
96+
- **Exports** → trait implementations on the module struct
97+
- **Zero-cost**: monomorphization, no vtables, no trait objects in hot paths
98+
- **WASI**: standard traits (`WasiFd`, `WasiPath`, `WasiClock`, `WasiRandom`) shipped with runtime
7599

76-
Each has its own:
77-
- **Globals struct** `G`: One typed field per mutable Wasm global; immutable globals are `const`
78-
- **Table**: Indirect call table with function references (for `call_indirect`)
100+
See SPECIFICATION.md §2.4–2.6.
79101

80-
Modules can call each other via trait-bounded functions. Memory ownership enforces spatial isolation — one module's memory is inaccessible to others.
102+
### Function calls
81103

82-
### Capability-based security via traits
104+
- **Direct** (`call`): regular Rust function calls with state threaded through
105+
- **Indirect** (`call_indirect`): safe static match dispatch over `func_index`, no function pointers
106+
- **Structural type equivalence**: canonical type index mapping at transpile time
83107

84-
**Imports** (what a module needs) become Rust trait bounds on generic host parameter `H`.
85-
**Exports** (what a module provides) become trait implementations.
108+
See SPECIFICATION.md §4.5.
86109

87-
Example:
88-
```rust
89-
// Module imports socket functions → requires SocketOps trait
90-
fn send<H: SocketOps + FileOps>(host: &mut H, ...) -> WasmResult<i32> { ... }
110+
### Error handling
91111

92-
// Module provides transform export → implements ImageLibExports
93-
impl ImageLibExports for ImageModule<MAX_PAGES> { ... }
94-
```
112+
- `WasmTrap` enum with 7 variants (OutOfBounds, DivisionByZero, IntegerOverflow, Unreachable, IndirectCallTypeMismatch, TableOutOfBounds, UndefinedElement)
113+
- `WasmResult<T> = Result<T, WasmTrap>` — no panics, no unwinding
114+
- `ConstructionError` for programming errors during module instantiation
95115

96-
**Zero-cost**: All dispatch via monomorphization (no vtables, no trait objects). If a module doesn't import a capability, the trait bound doesn't exist — no code path to call it.
116+
### Current status
97117

98-
WASI support is built-in via standard traits (`WasiFd`, `WasiPath`, `WasiClock`, `WasiRandom`, etc.) shipped with `herkos-runtime`. See SPECIFICATION.md §5 for complete details.
118+
- **Implemented**: Safe backend only (runtime bounds checking, no unsafe in output)
119+
- **Not yet implemented**: Verified backend, hybrid backend, `--max-pages` CLI effect, WASI traits
120+
- See `docs/FUTURE.md` for planned features
99121

100122
## `no_std` constraint
101123

102-
`herkos-runtime` and all transpiled output **must be `#![no_std]`**. No heap allocation without the optional `alloc` feature gate. No panics, no `format!`, no `String` in the runtime or generated code. Errors are `Result<T, WasmTrap>` only. The `herkos` CLI crate is standard `std` binary, this constraint applies only to the runtime and generated output.
124+
`herkos-runtime` and all transpiled output **must be `#![no_std]`**. No heap allocation without the optional `alloc` feature gate. No panics, no `format!`, no `String`. Errors are `Result<T, WasmTrap>` only. The `herkos` CLI crate is a standard `std` binary.
103125

104126
## Coding conventions
105127

106128
- **Rust edition**: 2021
107129
- **MSRV**: latest stable
108-
- **Error handling**: use `thiserror` for library errors, `anyhow` in CLI binaries. Wasm execution errors use the `WasmTrap` / `WasmResult<T>` types from the runtime crate (no panics, no unwinding).
109-
- **Naming**: follow Rust API guidelines. Wasm spec terminology (e.g., `i32.load`, `br_table`) maps to snake_case Rust (`i32_load`, `br_table`).
110-
- **Unsafe**: avoid `unsafe` in the runtime crate as much as possible — the whole point is compile-time safety. Any `unsafe` block requires a `// SAFETY:` comment explaining the invariant. In the verified backend output, `unsafe` blocks carry `// PROOF:` references to verification metadata instead.
111-
- **Tests**: unit tests live in `#[cfg(test)] mod tests` inside each module. Integration tests go in `tests/` directories per crate. End-to-end tests (Wasm → Rust → run) go in `tests/e2e/` at the workspace root.
112-
- **Dependencies**: keep the dependency tree small. Prefer `wasmparser` for Wasm parsing. Avoid pulling in a full Wasm runtime — we are the runtime. `herkos-runtime` must have zero dependencies in the default (no `alloc`) configuration.
113-
114-
## Function calls and indirect dispatch
115-
116-
### Direct calls (`call`)
117-
Transpile to regular Rust function calls with shared state (memory, globals, table) threaded through:
118-
```rust
119-
v5 = func_3(&mut memory, &mut globals, v3, v4)?;
120-
```
121-
122-
### Indirect calls (`call_indirect`)
123-
Implement safe dispatch via match statements. The transpiler:
124-
1. Looks up the table entry and validates its type
125-
2. Enumerates all functions matching the expected signature
126-
3. Emits a static match statement (becomes jump table in machine code)
127-
4. **No function pointers, no vtables, no dynamic dispatch** — 100% safe
128-
129-
Example:
130-
```rust
131-
let __entry = table.get(idx)?;
132-
if __entry.type_index != canonical_type {
133-
return Err(WasmTrap::IndirectCallTypeMismatch);
134-
}
135-
v4 = match __entry.func_index {
136-
0 => func_0(v0, v1),
137-
1 => func_1(v0, v1),
138-
_ => return Err(WasmTrap::UndefinedElement),
139-
};
140-
```
141-
142-
See SPECIFICATION.md §8.5 for structural type equivalence and table initialization details.
143-
144-
## Integration patterns
145-
146-
### Primary: Trait-based (Recommended)
147-
Host instantiates modules and provides capabilities through trait implementations:
148-
```rust
149-
struct MyHost { /* platform resources */ }
150-
impl SocketOps for MyHost { /* ... */ }
151-
impl WasiFd for MyHost { /* ... */ }
152-
153-
let mut module = Module::<MyGlobals, 256, 4>::new(16, MyGlobals::default(), table);
154-
let result = module.process_data(&mut MyHost::new(), ptr, len)?;
155-
```
156-
**Benefits**: Full type safety, zero `unsafe`, zero-cost dispatch via monomorphization.
157-
158-
### Alternative: C-Compatible ABI
159-
Optional `extern "C"` wrapper for integration with non-Rust systems. Erases generics using opaque types. See SPECIFICATION.md §10.2.
160-
161-
## Performance considerations
130+
- **Error handling**: `thiserror` for library errors, `anyhow` in CLI. Wasm errors use `WasmTrap`/`WasmResult<T>` (no panics, no unwinding).
131+
- **Naming**: Rust API guidelines. Wasm spec terminology maps to snake_case (`i32.load``i32_load`, `br_table``br_table`).
132+
- **Unsafe**: avoid in runtime crate. Any `unsafe` requires a `// SAFETY:` comment. In verified backend output (future): `// PROOF:` references.
133+
- **Tests**: unit tests in `#[cfg(test)] mod tests`. Integration tests in `tests/` per crate. E2E tests in `crates/herkos-tests/`.
134+
- **Dependencies**: minimal. `wasmparser` for parsing. `herkos-runtime` has zero dependencies in default config.
162135

163-
### Monomorphization bloat
164-
Each distinct `MAX_PAGES` and trait bound combination generates separate code. **Mitigation**:
136+
### Wasm parsing
165137

166-
1. **Outline pattern** (critical): Move logic into non-generic inner functions that take sizes as runtime parameters. Generic wrapper is a thin shell.
167-
```rust
168-
#[inline(never)]
169-
fn load_i32_inner(memory: &[u8], active_bytes: usize, offset: usize) -> WasmResult<i32> { ... }
138+
Use `wasmparser` only. Do NOT use `wasm-tools` or `walrus`. Emit Rust via string building or codegen IR — not `syn`/`quote`.
170139

171-
#[inline(always)]
172-
fn load_i32<const MAX_PAGES: usize>(mem: &IsolatedMemory<MAX_PAGES>, offset: usize) -> WasmResult<i32> {
173-
load_i32_inner(mem.pages.as_flattened(), mem.active_pages * PAGE_SIZE, offset)
174-
}
175-
```
140+
### Generated output conventions
176141

177-
2. **Normalize `MAX_PAGES`**: Use standard sizes (16, 64, 256, 1024) instead of exact declared maximums.
178-
179-
3. **Trait objects for cold paths**: Use `&mut dyn Trait` instead of generics for rarely-called code.
180-
181-
4. **LTO**: Link-time optimization eliminates unreachable monomorphized copies.
182-
183-
See docs/SPECIFICATION.md §13.3 for complete strategies.
184-
185-
### Parallelization
186-
The transpilation pipeline can be parallelized. IR building and code generation are embarrassingly parallel (each function is independent). The transpiler should use `rayon` for parallel iteration when processing modules with 20+ functions. See SPECIFICATION.md §13.5 for implementation details and performance expectations.
187-
188-
## Wasm parsing and code generation
189-
190-
### Parsing
191-
Use the `wasmparser` crate for reading `.wasm` binaries. Do NOT use `wasm-tools` or `walrus` unless there is a clear justification. The transpiler should operate on the structured output of `wasmparser` (types, functions, memory sections, etc.) and emit Rust source via string building or a small codegen IR — not via `syn`/`quote` procedural macro machinery.
192-
193-
### Generated Rust output
194-
Transpiled code should be:
195142
- Self-contained (only depends on `herkos-runtime`)
196143
- Formatted (run through `rustfmt`)
197-
- Readable and auditable — prefer clarity over compactness
198-
- No panics, no unwinding — use `Result<T, WasmTrap>` for error handling
144+
- Readable and auditable
145+
- No panics, no unwinding — `Result<T, WasmTrap>` only
146+
147+
### Performance considerations
148+
149+
- **Outline pattern** (mandatory for runtime): non-generic inner functions, generic wrapper is thin shell
150+
- **MAX_PAGES normalization**: standard sizes (16, 64, 256, 1024)
151+
- **Parallelization**: IR building and codegen are embarrassingly parallel (each function independent). Use `rayon` for 20+ functions.
199152

200153
## PR and commit guidelines
201154

202155
- Keep commits focused: one logical change per commit
203156
- Commit messages: imperative mood, short summary line, body if needed
204157
- All PRs must pass `cargo test`, `cargo clippy`, and `cargo fmt --check`
205-
- See docs/SPECIFICATION.md for the full technical specification of all components

CONTRIBUTING.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -192,7 +192,7 @@ Good commit messages:
192192
```
193193
feat: add support for multi-value blocks in IR builder
194194
195-
Implements multi-value block support as specified in SPECIFICATION.md §5.
195+
Implements multi-value block support as specified in SPECIFICATION.md §4.
196196
Adds tracking for block result types and proper stack management.
197197
198198
Closes #42
@@ -316,7 +316,7 @@ See [SECURITY.md](SECURITY.md) for responsible disclosure instructions.
316316
- Use the **outline pattern** for generic functions to prevent monomorphization bloat
317317
- Profile before optimizing (use `cargo bench` for microbenchmarks)
318318
- Document any performance-critical code sections
319-
- See SPECIFICATION.md §13.3 for monomorphization mitigation strategies
319+
- See SPECIFICATION.md §6.2 for monomorphization mitigation strategies
320320

321321
## Questions?
322322

crates/herkos-runtime/KANI.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -127,5 +127,5 @@ mod proofs {
127127

128128
- [Kani Tutorial](https://model-checking.github.io/kani/kani-tutorial.html)
129129
- [Kani Rust Book](https://model-checking.github.io/kani/)
130-
- [SPECIFICATION.md §9.4](../../SPECIFICATION.md) — Contract-based verification design
131-
- [SPECIFICATION.md §11.3](../../SPECIFICATION.md) — Runtime verification requirements
130+
- [FUTURE.md §4](../../docs/FUTURE.md) — Contract-based verification design
131+
- [SPECIFICATION.md §3.2](../../docs/SPECIFICATION.md) — Runtime architecture

0 commit comments

Comments
 (0)