Menu
WASM engine features, proposition deciding, and WASM memory configuration
Install with Codex or Claude Copy this prompt, paste it into Codex, Claude, or another assistant, and let it review the skill page and install it for you.
Based on SOC occupation classification
Catalogue of every covalence-* crate — what each one wraps/provides and which layer it lives in. Consult when deciding which crate to use, where new code belongs, or how the workspace is structured.
Performance of the Metamath → HOL import (covalence-metamath + covalence-hol metalogic) — pipeline, hotspots, the bench, and the history of super-linearity fixes
How to profile and optimize covalence — flamegraphs, callgrind/cachegrind, and the scaling-first methodology for finding super-linear work
VSCode extension architecture and LSP server details
Covalence repo layout, dependency graph, and key architectural rules
Performance of the Metamath → HOL import (covalence-metamath + covalence-hol metalogic) — pipeline, hotspots, the bench, and the history of super-linearity fixes
| name | wasm-guide |
| description | WASM engine features, proposition deciding, and WASM memory configuration |
| disable-model-invocation | true |
covalence-wasm featuresvalidate::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.
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.decide command, but the corresponding handler is gone.When/if proposition deciding returns, re-document it here.
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.