Context
We are introducing Schema 2.0 for probe output files (probe-lean, probe-verus). The key changes are:
-
Envelope wrapper: All probe JSON outputs will be wrapped in a metadata envelope instead of being bare dictionaries. The envelope contains schema, schema-version, tool (name, version, command), source (repo, commit, language, package, package-version), timestamp, and data.
-
Folder restructure: The flat .verilib/ layout is being reorganized into subdirectories:
Current:
.verilib/
config.json
atoms.json
specs.json
proofs.json
stubs.json
graph.json
structure/
Proposed:
.verilib/
config.json
probes/
lean_<package>_<version>.json
verus_<package>_<version>.json
views/
molecule_all.json (replaces stubs.json)
package_all.json
translations/
verus_dalek__lean_dalek.json
What needs to change in verilib-cli
1. Read enveloped probe outputs
All code that reads atoms.json, specs.json, proofs.json needs to:
- Expect the data under a
"data" key inside an envelope object
- Optionally validate
schema and schema-version fields for compatibility
- Read from
probes/ subdirectory instead of flat .verilib/ root
Affected files:
src/commands/atomize.rs (reads atoms.json)
src/commands/specify.rs (reads specs.json)
src/commands/verify.rs (reads proofs.json)
src/config.rs (atoms_path(), stubs_path(), verilib_path())
2. Write to new folder structure
init should create probes/, views/, translations/ subdirectories
- Output paths should target the new locations
deploy should scan the new folder structure
3. Use envelope metadata for staleness detection
The source.commit and timestamp fields in the envelope enable checking whether probe outputs are stale relative to the current repo HEAD. This supports the workflow: "commit before atomize/specify/verify; if not committed, regenerate everything."
4. Views replace stubs
stubs.json becomes a "view" in views/molecule_all.json. The stubify concept evolves into a filtered projection of probe data.
Design documents
Notes
- No backward compatibility period needed -- probe tools and verilib-cli are updated in lockstep
- Each probe file is self-describing via its envelope, so verilib-cli can dispatch on content rather than filename/path
- The filename convention
<language>_<package>_<version>.json is for human convenience; code should read the envelope
Context
We are introducing Schema 2.0 for probe output files (probe-lean, probe-verus). The key changes are:
Envelope wrapper: All probe JSON outputs will be wrapped in a metadata envelope instead of being bare dictionaries. The envelope contains
schema,schema-version,tool(name, version, command),source(repo, commit, language, package, package-version),timestamp, anddata.Folder restructure: The flat
.verilib/layout is being reorganized into subdirectories:Current:
Proposed:
What needs to change in verilib-cli
1. Read enveloped probe outputs
All code that reads
atoms.json,specs.json,proofs.jsonneeds to:"data"key inside an envelope objectschemaandschema-versionfields for compatibilityprobes/subdirectory instead of flat.verilib/rootAffected files:
src/commands/atomize.rs(reads atoms.json)src/commands/specify.rs(reads specs.json)src/commands/verify.rs(reads proofs.json)src/config.rs(atoms_path(),stubs_path(),verilib_path())2. Write to new folder structure
initshould createprobes/,views/,translations/subdirectoriesdeployshould scan the new folder structure3. Use envelope metadata for staleness detection
The
source.commitandtimestampfields in the envelope enable checking whether probe outputs are stale relative to the current repo HEAD. This supports the workflow: "commit before atomize/specify/verify; if not committed, regenerate everything."4. Views replace stubs
stubs.jsonbecomes a "view" inviews/molecule_all.json. The stubify concept evolves into a filtered projection of probe data.Design documents
Notes
<language>_<package>_<version>.jsonis for human convenience; code should read the envelope