Skip to content

JSON mapping

All probes emit a Schema 3.0 envelope. Canonical field docs: probe SCHEMA.md.

Envelope

Field Role
schema e.g. probe-verus/extract
schema-version "3.0"
tool name / version / command
source repo, commit, language, package (probe-aeneas uses inputs instead)
timestamp ISO-8601
data Map of probe-id → atom object

Atomize plugins read data into ParsedAtoms / Atom instances, then persistence writes MySQL atoms, atomsdependencies, snippets, and verification fields.

Atom fields (summary)

Required in probe JSON: display-name, dependencies, code-module, code-path, code-text (lines-start / lines-end), kind, language.
Optional: verification-status, primary-spec, untracked, Lean specs / specified.

Kinds differ by language (Verus exec/spec/proof; Lean def/theorem/…). Aeneas merges Rust + Lean atoms with cross-language edges (linetype dashed vs full in DB).

Per-probe schemas

The hub spec defines the shared contract; each probe's language-specific fields and schema values are canonically documented in its own repo's docs/SCHEMA.md:

Probe Emits (schema values) Canonical spec
probe (hub) probe/merged-* (merged envelopes) probe SCHEMA.md — the interchange spec
probe-verus probe-verus/extract + per-step atoms / specs / proofs / verification-report / extract-summary / stubs probe-verus SCHEMA.md
probe-lean probe-lean/extract, probe-lean/viewify probe-lean SCHEMA.md
probe-aeneas probe-aeneas/extract, probe/mappings probe-aeneas SCHEMA.md
probe-rust probe-rust/extract probe-rust SCHEMA.md
probe-leanblueprint probe-leanblueprint/extract, probe-leanblueprint/summary (sidecar, never merged) probe-leanblueprint SCHEMA.md

The atomizer currently ingests the probe-verus, probe-lean, and probe-aeneas extracts (see languages and plugins); probe-rust is a tool-level member of the family, and probe-leanblueprint's enriched extract adds language: "blueprint" node atoms not yet ingested.

Connecting atoms across languages

Three atom pairings occur in probe extracts, one per subsection below. Two conventions hold everywhere:

  • Every list field means "depends on / uses" — the atom carrying the field points at what it needs — so arrows are drawn from the atom to the atoms it lists, one direction convention per canvas.
  • Where two layers genuinely exist, one field is the pointer to the counterpart (translation-name for Aeneas, blueprint-label for blueprints) and dependencies carries the cross-layer edges; Verus is the deliberate exception — one layer, no counterpart to point at.

Rust and Lean atoms (Aeneas)

A probe-aeneas/extract carries a genuine two-layer pairing: compiled Rust functions (language: "rust", kind exec) and their Aeneas-generated Lean translations (language: "lean"). Canonical semantics: probe-aeneas SCHEMA.md.

flowchart LR
  subgraph rust ["Rust layer — language: rust"]
    R1["probe:crate/0.1.0/mod/f()"]
    R2["probe:crate/0.1.0/mod/g()"]
  end
  subgraph lean2 ["Lean layer — language: lean"]
    T1["probe:Crate.f"]
    T2["probe:Crate.g"]
  end
  R1 -- "1 · dependencies" --> R2
  T1 -- "1 · dependencies" --> T2
  R1 -. "2 · translation-name" .-> T1
  R1 -- "3 · dependencies (cross-language)" --> T2
# From → To Field on the from atom Meaning
1 same-language dependencies the call graph within each layer
2 rust → lean translation-name (+ translation-path / translation-text) the function's primary Lean translation (1-to-1)
3 cross-language dependencies (mixed keys) merge-added edges: for each dependency with a known translation, the translated code-name is added as an extra dependency, in both directions — these are the edges the frontend draws dashed (linetype)

Also on the Lean side: rust-source holds the originating Rust path (parsed from the Aeneas docstring — a file reference, not an atom key). The full Rust↔Lean mapping with per-entry confidence × method lives in the separate probe/mappings output of probe-aeneas translate.

Rust and Verus atoms

Verus needs no counterpart pointer — unlike Aeneas there are not two parallel worlds to stitch. exec, spec, and proof atoms live in the same source files and the same code-name namespace, differing only by kind (language is derived from it: exec → "rust", spec/proof → "verus"):

flowchart LR
  subgraph one ["One layer — kinds within the same namespace"]
    E["exec probe:crate/0.1.0/mod/f()"]
    S["spec probe:crate/0.1.0/mod/f_spec()"]
    P["proof probe:crate/0.1.0/mod/f_correct()"]
  end
  E -- "requires-dependencies" --> S
  P -- "body-dependencies" --> E
  P -- "body-dependencies" --> S

Their connection is the ordinary dependency graph, refined by where each edge occurs:

Field on the from atom Meaning
dependencies the call graph, naturally cross-kind (an exec function referencing a spec fn in its contract, a proof referencing both)
requires-dependencies / ensures-dependencies / body-dependencies that same list partitioned by call site — contract vs body (the Verus analog of Lean's type-/term-dependencies)
dependencies-with-locations per-edge precondition / postcondition / inner tags (opt-in --with-locations)

The spec itself is embedded, not linked: an exec atom's primary-spec holds the full requires/ensures text (contrast probe-lean, where primary-spec is a code-name — see the polymorphism note in the per-probe table), and verification results merge into the exec atom's verification-status rather than appearing as edges. Canonical: probe-verus SCHEMA.md.

Lean and blueprint atoms

A probe-leanblueprint/extract carries two atom layers — the Lean code layer (language: "lean") and the blueprint/paper layer (language: "blueprint", one node atom per blueprint node, keyed probe:blueprint:<label>), connected by four edge kinds. Canonical semantics: probe-leanblueprint SCHEMA.md §Node atoms.

flowchart LR
  subgraph paper ["Paper layer — language: blueprint"]
    N1["probe:blueprint:thm_main"]
    N2["probe:blueprint:lemma_helper"]
  end
  subgraph code ["Code layer — language: lean"]
    L1["probe:Foo.main_theorem"]
    L2["probe:Foo.helper"]
  end
  N1 -- "2 · blueprint-*-uses" --> N2
  L1 -- "1 · dependencies" --> L2
  N1 -- "4 · dependencies (binding)" --> L1
  L1 -. "3 · blueprint-label" .-> N1
# From → To Field on the from atom Meaning
1 lean → lean dependencies (typed split: type-dependencies / term-dependencies) the code graph: decl uses decl
2 node → node blueprint-statement-uses / blueprint-proof-uses (values are probe:blueprint:* keys) the paper graph: closed over node atoms, mirrors the blueprint's own dependency graph
3 lean → node blueprint-label (a label string; the node atom's key is "probe:blueprint:" + label) this decl is bound by that node — the ownership winner under collisions
4 node → lean dependencies on a bound node atom (values are probe:* Lean keys) the node's claimed binding: the decls that back it

Rules a consumer must follow:

  • Edges 3 and 4 are not inverses. Under a binding collision, a losing node atom still lists the decl in its dependencies (its claim), while the decl's blueprint-label names the winning node. Never derive one edge by inverting the other.
  • The uses fields are class-dependent. On node atoms, blueprint-statement-uses/-proof-uses resolve node-to-node (edge 2); the same field names on enriched Lean atoms keep the historical resolution to code representatives. Build the paper graph from node atoms only.
  • One layer per view, never summed. Code-level stats and graphs read language: "lean" atoms + edge 1; blueprint progress and the paper graph read node atoms + edge 2; edges 3–4 are the cross-layer stitching for a combined view. A bound node atom's verification-status mirrors decls already counted on the Lean side.
  • Displaying a node (probe-leanblueprint ≥ 0.8.0): a node atom carries its statement as authored in blueprint-statement-text (+ -format, untrusted source markup — escape or sandbox) and its declaration site in blueprint-source-path / blueprint-source-lines for click-through; both are optional and independent.

Output paths

Probe JSON is expected under the cloned repo at .verilib/probes/<lang>_*.json (see languages and plugins).