メニュー
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.
Codex または Claude でインストール この Prompt をコピーして Codex、Claude、または他のアシスタントに貼り付けると、Skill ページを確認してインストールできます。
SOC 職業分類に基づく
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
How to profile and optimize covalence — flamegraphs, callgrind/cachegrind, and the scaling-first methodology for finding super-linear work
| name | crate-map |
| description | 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. |
| disable-model-invocation | true |
The workspace is many covalence-* crates. Dependency discipline: all use of
an external library goes through its wrapper crate — never import the underlying
dep directly (so deps are centralized and extensible without touching every
consumer). The layers below mirror the dependency stack (see
notes/vibes/crate-graph.md) and the in-flight three-layer reorg (notes/vibes/refactor-plan.md).
wat, wasmparser, wasmprinter, wasm-encoder, optionally wasmtime (runtime feature; re-exported via engine::wasmtime). ModuleBuilder, Val/ValType.blake3, sha2, optionally gix-hash (git feature). O256 hash, HashCtx (BLAKE3/SHA-256/git), ContentHash/ContentId, CovRoot domain-separated hashing.rusqlite; open()/open_memory() with WAL + NORMAL sync + busy-timeout pragmas.rand. All randomness goes through here.proptest (property-based testing). Dev-dependency consumers only — must never appear on a non-dev edge (kept out of docs/deps/tcb.json that way). Use via use covalence_proptest::proptest::prelude::*; so the proptest! macros resolve.ed25519-dalek (EdDSA). Re-exports pinned rand_core 0.6 as dalek_rand_core (the one exception to the covalence-rand rule).winnow; leb128 module (unsigned LEB128 varints).SExp<A>; default SExpr = SExp<Atom> (Symbol(SmolStr) | Str{format,bytes}). Layers: SExpVisitor (SAX + dialect), SExpBuilder/TreeBuilder, SExp. Dialects: CovalenceDialect (;;, (; ;), |...|), SmtLibDialect, WatDialect. parse()/parse_smt()/parse_wat()/parse_with(); map()/map_ref().Decision (sat/unknown/unsat), Bits, and (default int feature) Nat/Int arbitrary-precision (wraps num-bigint/num-traits/num-integer), Sign, errors. Nat subtraction saturates; use checked_sub.wasm feature.arrow; parse_ipc() (auto file vs stream) → ArrowInfo.parquet; parse_file(), scan_hive() (decoupled via HiveSource).cyruscook/spectec_parse (ast/decode/decode_derive/wasm). wasm::get_wasm_spectec_ast() returns the WASM 3.0 spec as a SpecTec AST. Untrusted driver lowering WASM semantics into HOL.Graph<P>/GraphBuilder<P>, BytesGraph), LabelList/KindFlags overlays, StringDiagram, cov:graph@0.1.0 WIT, pure-Rust render_svg. Symmetric premonoidal: insertion order = init order; linear inputs, fan-out outputs.serde_json only (serde itself stays a normal direct dep).crates/lang/inductive) — the logic-agnostic inductive-types API: plain-data InductiveSpec<X> (simple = single/non-indexed/strictly-positive/first-order), two-tier Logic/LogicOps abstraction, InductiveTheory/InductiveFacts bundle (membership-relativized contract, iteration recursor, rule-form schematic theorems, honest BackendCaps), InductiveBackend seam, generic conformance suite. Deps: smol_str+thiserror only. HOL backends live in covalence-init::init::inductive::{api,church,engine,carved}: impredicative Church (church) = universal, no cdr (any spec incl. the sexpr flagship, catamorphic recursor, rec_injective=false); carved = exact, full-Lisp (the atom|snil|scons shape via new_type_definition, paramorphic recursor + car/cdr/rec-injectivity); engine adapter (engine) = exact nat; a set.mm backend slots in later. The Lisp theory (init::lisp, Lisp) is the first carved consumer — car/cdr/cons/consp/atom?/len/append + append_assoc/len_append by structural induction (ACL2 groundwork). Design + universal-vs-exact split + proof/acl2 frontend map: notes/vibes/inductive-api-design.md (§4, §10).ContentStore, BlobStore, TaggedStore/TaggedBlobStore, ObjectStore/KeyedObjectStore, GitPrefixStore, SharedMemoryStore, KvStore, SqliteStore (sqlite feature). Must stay portable to wasm32-wasip1-threads.Dir/DirBuilder, Table/TableBuilder (LEB128 rows), git tree-format conversion.hash_blob, loose/odb backends, Git LFS.cov:kv@0.1.0).Schema::builder (olog: objects, morphisms, attributes, path equations) + check; Instance (order-independent add_part→Part, set_hom/set_attr, follow) + validate (functoriality + equations), acyclic, attr_injective; Functor + Instance::pullback (Δ functorial data migration); AttrVal typed attributes; query (Query::builder conjunctive queries — answers = homomorphisms, join-style backtracking); datalog (Program/Rule recursive queries — derived relations to a least fixpoint, e.g. transitive closure); lattice (JoinSemilattice + lfp = Datafun's fix; MinDist for min-plus, set/map/bool instances — set-valued and lattice-valued recursion through one combinator; the Datafun seam is notes/vibes/sketches/acset-datalog-datafun.md). Used by covalence-multiformat.Cid (blake3 multihash, base16 multibase), codec content-type registry, DerivationFact envelope (reifies the waist existential), FactStore::check (proof-checking as a constraint query), identity::covalence_name (verified wire CID ↦ COV_ROOT Name256), acset (the interchange schema + validate_store, built on covalence-acset — structural/meta-theoretic validation of a FactStore, native to a geometric kernel). Wire layer only — logical payloads stay opaque; the kernel_ingest example (dev-dep on covalence-init) binds an envelope to a real covalence-core Thm. See crates/lib/data/multiformat/SKELETONS.md.crates/kernel/base) — closed-world equality kernel (Stage 0 built: Thm<L,P> LCF certificate, Op/Expr/Eqn, parameter-free Language) — facade over covalence-pure-trusted; covalence-core builds on it. See notes/vibes/closed-world-kernel.md.crates/kernel/base/trusted) — the TCB floor: the trusted closed-world kernel internals covalence-pure re-exports.crates/kernel/base/eval) — the Builtins base language: every native computation the kernel will ever trust, as per-op Op+CanonRule ZSTs over covalence_types (nat/int/bytes + the u8…s64 fixed-width families), semantics transcribed from covalence-core's builtins.rs (incl. the FORCED n mod 0 = n, x/0 = 0, x rem 0 = x), pinned by a differential suite + the MANIFEST golden docs/deps/builtins-manifest.txt (regen: COV_REGEN_GOLDEN=1). Deps: covalence-pure + covalence-types ONLY — the -> covalence-core edge is BANNED in dep-graph; enters the TCB when core opens the seam (toHOL purge S4).covalence-pure(-trusted) (safe Rust; core::Thm<L: HolTier = CoreLang> is a newtype over pure::Thm — see docs/deps/tcb.json; Thm<CoreLang> carries NO computation axioms). HOL-Light-style kernel, locally-nameless Term/Type. Logical primitives are only = (TermKind::Eq) and ε (TermKind::Select); connectives — including T/F themselves since EG3b (tru ≡ (λp.p)=(λp.p), fal ≡ ∀p:bool.p) — are defined constants in defs/logic.rs. HOL Light's equality-core primitives + a few fast derived constructors with Soundness: docstrings (25 rules, golden docs/deps/core-manifest.txt — the connective/quantifier rules, lem (L2) and false_elim (EG3b) left the kernel: they are zero-TCB, tier-generic derivations in covalence-hol-eval::derived::DerivedRules, same signatures, working at Thm<CoreLang> and EvalThm alike; the transitional Bool literals ⌜T⌝/⌜F⌝ bridge to the defined T/F via derived eval-tier equations in covalence-hol-eval::boolean); define + new_type_definition (returns the bijection as ONE unsplit conjunction — split via eval's TypeDefExt); unfold_term_spec; spec_abs/spec_rep. Two non-computational primitive rules: nat_induct (sequent form), unit_eq. src/defs/ is only the D3 residue (literal-leaf type handles + connective builders — dies with the literal leaves; see its SKELETONS.md): the term-op catalogue and the cert rules moved to covalence-hol-eval (stage E2). Read notes/vibes/kernel-design.md before touching.crates/kernel/hol/eval) — the eval tier: owns CoreEval (a Language extending CoreLang) + EvalThm = Thm<CoreEval>; hosts the per-family computation certificate rules + toHOL rules (rules.rs, 17 rules incl. FloatCert, golden docs/deps/eval-manifest.txt) NEXT TO their defs/ dispatch tables and the term-op catalogue (the auditability goal — defs/floats.rs = the two-layer float architecture: F2b bit-level declarations + the F2c typed f64.* let-style wrappers). Trust is per-rule via admits; the drivers (reduce/prove_true/delta, the lit.rs facade, the typed_float.rs composite that reduces typed float ops with NO new rule) stay untrusted. derived.rs (stage L2) = the zero-TCB connective/quantifier rules (DerivedRules — drop-in signatures for the deleted kernel rules incl. lem via a cached ε-schema; TypeDefExt splits the typedef bijection); eval-tier only because ⊢ T needs the cert path. GOTCHA: reduce's normal forms are load-bearing for hand-assembled trans chains in covalence-init — never widen its catalogue over existing symbols (new opt-in passes instead; see init/ball.rs's ball_eval + ext::fire_all). tests/pure_hol_units.rs = the definition-vs-native differential per cert family (dev-dep on covalence-init). core -> hol-eval and normal hol-eval -> init are BANNED dep-graph edges.HolLightCtx + the HolLightKernel/HolLightTerms/HolLightTypes traits + shared NameId/HolError types. The surface HOL proof consumers (covalence-init, the OpenTheory importer) build against. Depends only on covalence-core.Thm alias is covalence_hol_eval::EvalThm): the init/ theory catalogue, proofs/ tactics, the script/ .cov layer + project, metalogic/peano (Metamath bridge), models, grammar/{regex,spectec} grammars, the algebra theories, hash/sexp. Depends on covalence-hol and re-exports its surface (so covalence_init::{HolLightCtx,traits,types,Term,…} resolve)..mm reader, Database. covalence-init consumes it.crates/kernel/core) — the "OS-kernel" layer over the logical TCB: sits between covalence-init and covalence-shell, wiring the HOL proof world to durable infrastructure. Re-exports covalence_init; backend (SyncBackend/AsyncBackend/KernelError), store (a content-addressed Kernel over the blob store), service (KernelService), and a skeleton facts module (the observer layer lands here). See crates/kernel/core/src/lib.rs.crates/kernel/hol/api) — the TRAIT-backed consumer surface (non-TCB, zero delta): Hol (value-typed HOL Light), Nat, Int (the abstracted integer API — builders + destructors + ordered-ring lemma accessors), HolOmega; NativeHol is the only impl naming the concrete backend. Point: swap the backend / integer representation by writing one impl. Consumed by lang/lisp, lang/haskell, kernel/web, and (planned) the SMT replay.crates/kernel/sat) — generic SAT-proof replay (UNTRUSTED, zero TCB): the ClauseBackend resolution seam + replay_lrat, turning a DRAT/LRAT refutation (from lib/sat) into backend theorems. The propositional substrate for the SMT replay.crates/kernel/smt) — generic SMT-proof replay (UNTRUSTED, zero TCB): the pure Farkas certificate checker (rational/lincomb/farkas — Alethe la_generic linear algebra, backend-independent) + RulePolicy (admit only a subset of Alethe). Written over covalence-hol-api::Int, so it retargets HOL / alt-int-reps / internal-PA / SOA. Turns a parsed Alethe proof (lib/smt) into ⊢ ⊥. See notes/vibes/logics/smt-import-architecture.md.AletheBridge + HolAletheBridge + ingest + la.rs Farkas + (#by (smt)) tactic). The working HOL bridge; its generic, backend-parameterised successor is covalence-kernel-smt (migration pending).external-egglog feature — released egglog still lacks the proof module; see the crate's Cargo.toml).ArticleInterp<K: HolLightKernel> (the trait is the backend-swap seam) + a native backend NativeOt (feature native) over covalence-core — zero TCB beyond core HOL (axioms are hypothesis-tracked assumes, never minted). Package/dep resolution + offline FileResolver / HTTP-cache CachingUrlResolver (feature fetch). Driven by cov hol check <files.art> / cov hol pkg <packages> and bun run opentheory[:offline] (download+cache+verify-all bench). The online resolver versions bare names via the repo's ?pkg= page, so the whole stdlib verifies: cov hol pkg base = 1340 theorems (~46s cached). A reusable matching framework (matching.rs: MatchLogic × MatchStrategy) + native-override system (NativeOverrides/OverrideMap) discharge OpenTheory's axioms natively: cov hol pkg --native-axioms base proves infinity (over nat), extensionality, and choice in covalence's kernel → 1340 theorems relative to ZERO axioms (axioms.rs). Design: notes/vibes/logics/opentheory-import.md; open work in the crate's SKELETONS.md (.int interpretations).crates/lang/haskell) — small Haskell-dialect surface built as the pipeline Haskell ⇒ SExpr IR ⇒ backend: hand-rolled parser, crate-local sexpr interchange IR (canonical text printer/parser; nat atoms = covalence-types Nat, arbitrary precision), ONE canonical desugaring (lower), pluggable Realize backend seam (realize; demo backends in backends), and a hol-feature backend realizing the IR as carved sexpr kernel Terms (atom payloads via covalence_hol_eval::mk_blob — keep the purge ratchet at 0). The "write init/ in the dialect" on-ramp; flagship demo tests/init_dialect.rs.crates/lang/k) — the K-framework frontend. Untrusted, kernel-free, #![forbid(unsafe_code)]. Two independent frontends: (1) KORE (ast/parse/sexpr/fragment) — consumes the elaborated matching-logic IR kompile emits as definition.kore (as covalence-spectec consumes elaborated SpecTec AST): parser (mangled identifiers, multiary \and/\or, sortless \mu/\nu), canonical S-expr IR, and the fragment classifier (rewrite/function/subsort/constructor/… ladder, RewriteRule extraction). (2) .k-source grammar (kdef) — reads a K definition's syntax (BNF) declarations directly, skipping rule/configuration/… sentences: a winnow-based parser (kdef::parse, via covalence_parse::winnow) for modules/imports/productions/|/> priority/[attrs]/List{}, a canonical S-expr IR (kdef::sexpr), and a lowering to covalence_grammar::Cfg (kdef::cfg) that feeds the kernel CFG stratum. Imported builtin sorts (Id/Int/Bool from DOMAINS-SYNTAX) resolve via the swappable cfg::SortResolver trait (NoDomains = structural, KDomains = K builtin token regexes). Parses the real LAMBDA/IMP tutorial grammars (vendored BSD-3 in examples/k-tutorial/). Deps: covalence-sexp, covalence-grammar, covalence-parse, smol_str, thiserror. The F0 KORE→Derivable_KStep lowering lives in covalence-init::k; design notes/design/k-frontend.md.cov CLI (clap 4 + color-eyre).lsp-server 0.7 + lsp-types 0.97).cog command).