wasm-guide

name	wasm-guide
description	WASM engine features, proposition deciding, and WASM memory configuration
disable-model-invocation	true

covalence-wasm features

• Base (no features) — WAT validation (validate::compile_wat, validate::wasm_to_wat), binary parsing (parse::parse_module, parse::parse_component), component encoding (component::encode_core_as_component), programmatic module construction (build::*, ~840 LoC). Returns typed WasmError. Depends on wat, wasmprinter, wasmparser, wasm-encoder, wit-component, wit-parser. WASM-safe (compiles to wasm32-wasip1-threads).
• runtime (non-default) — re-exports the full wasmtime crate via src/engine.rs (pub use wasmtime;), AND provides a WIT-shaped runtime trait in src/runtime.rs generated by wasmtime::component::bindgen! from wit/cov-wasm.wit (package cov:wasm@0.1.0, interface runtime, world cov-wasm-guest). The trait surface is compile/instantiate/call-u32 over component/instance resources; RuntimeHost is the wasmtime-backed impl. Direct wasmtime use stays alongside for fuzz/perf consumers (covalence-sat, covalence-wasm-spec). Not WASM-compatible (native only).

The same conceptual surface is mirrored in TypeScript at packages/covalence-wasm-js/src/index.ts (Runtime class). MVP supports core modules only via WebAssembly.compile / WebAssembly.instantiate; component bytes throw with a pointer at the jco follow-up (proposal Phase 3.1+). Run with bun run test:wasm-js.

The Val/ValType types in src/val.rs are engine-agnostic and are the intended lingua franca for any future multi-backend runtime trait.

Proposition Deciding

Status: not currently implemented in any Rust crate. Earlier kernel iterations included a decide function that asked "does this proposition WASM component call attest()", but no such Rust API exists in this branch — grep -rn "fn decide" crates/ returns nothing. The current covalence-kernel is a HOL kernel (see crates/kernel/core/src/{arena,prop,thm,...}.rs).

References that remain:

• crates/ffi/python/covalence.pyi declares a decide Python API (planned/external).
• crates/lib/types/src/decision.rs has the Decision three-valued type used by SAT/SMT crates.
• The REPL highlight list still names a decide command, but the corresponding handler is gone.

When/if proposition deciding returns, re-document it here.

WASM Memory

The desktop/web VSCode extension runs cov.wasm as a WASI process with a fixed 2 GB linear memory. The size must match in two places:

• extensions/covalence-vscode/scripts/build.ts — WASM_MEMORY_BYTES = 32768 * 65536 (2 GB) is passed to the linker via --initial-memory / --max-memory.
• extensions/covalence-vscode/src/server.ts — wasm.createProcess(... { initial: 32768, maximum: 32768, shared: true }) (page count).

Because this is shared memory (SharedArrayBuffer), the full 2 GB is reserved as virtual address space. On Linux, physical RAM is only committed for pages actually touched (overcommit). On Windows, the full size may count against the system commit charge.