Menu
WASM engine features, proposition deciding, and WASM memory configuration
Instalar com Codex ou Claude Copie este prompt, cole no Codex, Claude ou outro assistente e deixe que ele revise a página da skill e instale para você.
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
Baseado na classificação ocupacional SOC
| 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.