Proof coverage: 45/70 functions matched — two gaps to close

[astefano]

Summary

The Z3 proof certificate pipeline successfully generates proofs for 45 out of 70 verified functions in pmemlog. There are two separate gaps in the pipeline that account for the missing 25 functions.

The numbers

Stage	Count	Source
Verus total functions	109	Verus compiler output
Verus verified	72	Verus compiler output
results.json entries	48	probe-verus verify (atomized)
Matched to .smt2	45	proofs.py name mapping
.smt2 files produced	93	Verus -V spinoff-all

Gap 1: Verus 72 verified → results.json 48 entries

probe-verus only includes functions that go through its atomize pipeline (call graph analysis via verus-analyzer). Functions that aren't reachable in the call graph or that verus-analyzer can't resolve get filtered out. Known categories of missed functions:

• Trait default method implementations
• Certain macro-generated functions
• Closures and anonymous functions
• Functions not reachable from the analysis entry points

Impact: 24 verified functions are not in results.json at all, so they can't appear in the proof bundle.

Fix: Improve probe-verus coverage — either by enhancing verus-analyzer symbol resolution or by falling back to Verus's own function list when atomize misses functions.

Gap 2: results.json 48 → matched to .smt2 45

3 functions in results.json couldn't be mapped to any .smt2 file. The mapping logic in proofs.py normalises both:

• The probe-verus key (e.g., probe:pmemlog/0.1.0/logimpl_v/...#untrusted_append())
• The Verus internal name from the .smt2 Function-Def comment (e.g., lib::logimpl_v::UntrustedLogImpl::untrusted_append)

Matching fails when:

• Function names get mangled differently (generics, closures, impl blocks)
• The module path parsed from the probe key doesn't align with the Verus namespace
• A function has multiple .smt2 files (spinoff variants) and module context isn't enough to disambiguate

Impact: 3 functions have entries in proofs.json but with z3_formula: null and z3_proof: null.

Fix: Improve build_function_mapping() in proofs.py:

• Add Levenshtein/fuzzy matching as a fallback
• Use the full Verus qualified name (not just the leaf) for matching
• Have Verus emit a canonical function ID in .smt2 comments (upstream)

Important note

All 93 .smt2 files are still produced and available. The proof evidence exists — we just can't automatically associate 25 of the functions with their corresponding .smt2 files yet. This is a mapping/coverage issue, not a data loss issue.

Labels

• enhancement
• proof-pipeline

[astefano]

Update: March 2026 — coverage data for pmemlog + dalek

We now have proof bundle data for both certified projects. The picture has changed significantly since the original issue was filed.

pmemlog (latest certification: 2026-03-23)

Stage	Count
Verus verified	72
results.json entries	70 (all verified)
proofs.json entries	66 (all matched to .smt2)
Z3 proofs generated	66 (100% success)

Gap 1 (72 → 70): 2 functions not captured by probe-verus atomize.
Gap 2 (70 → 66): 4 functions are axioms/mocks/spec-fns (axiom_bytes_uncorrupted, axiom_corruption_detecting_boolean, bytes_crc, VolatileMemoryMockingPersistentMemory::new). Verus accepts these on trust — no .smt2 file is emitted. This is correct behavior.
Gap 3: none. All 66 matched functions produce Z3 proofs.

Coverage improved from 45 → 66 entries between Feb and Mar, reflecting probe-verus improvements.

curve25519-dalek (latest certification: 2026-03-22)

Stage	Count
Verus verified	1157 / 1208 total
results.json entries	1199 (1150 verified)
proofs.json entries	1130 (all matched to .smt2)
Z3 proofs generated	1110
Z3 proof errors	20 (all "unknown")

Gap 2 (1199 → 1130): 69 verified functions not in proof bundle. Breakdown by category:

Module	Count	Nature
subtle_assumes	26	Trusted axioms for constant-time operations
core_assumes	18	Trusted axioms for Rust core byte conversions
iterator_specs	10	Iterator specification stubs
Other (lizard_ristretto, ristretto, scalar, traits, scalar_helpers, edwards)	15	Various trusted/extern functions

These are all trusted external function axioms — Verus verifies them by assumption, no SMT query is generated. This is not a matching failure.

Gap 3 (1130 → 1110): 20 functions where Z3 returns "unknown" with legacy proof mode. These are complex cryptographic lemmas (batch compress, montgomery reduce, pippenger, scalar multiply, etc.) where (set-option :proof true) changes Z3's solver heuristics enough that the queries become undecidable within the 300s timeout. Verus confirms they pass without proof production.

Revised assessment of the two original gaps

Original Gap 1 (Verus 72 → results.json 48): Substantially closed. pmemlog now has 70/72 in results.json (was 48). The 45→66 jump in proof bundle entries reflects this improvement.

Original Gap 2 (results.json 48 → matched 45, 3 unmatched): Resolved. Current data shows 0 name-matching failures for both projects. All functions that have an .smt2 file are matched correctly by build_function_mapping(). The 3 originally unmatched functions were resolved by the probe-verus coverage improvements.

New gap type: Gap 3 (Z3 proof production failures)

Not in the original issue. 20 dalek functions have .smt2 formulas but Z3 legacy proof mode cannot produce proofs for them. This is a Z3 solver limitation, not a pipeline bug.

Recommended next steps

1. Mark trusted axioms explicitly in proofs.json (e.g., "status": "trusted-axiom") — low effort, clarifies why functions are absent
2. Investigate Z3 options for the 20 dalek failures — medium effort, could improve proof coverage from 98.2% to 100%
3. Record Verus raw function counts in history.json — low effort, enables precise Gap 1 measurement
4. Consider closing or downgrading the C2 (name-matching) known bug — 0 current failures

Full analysis: kb/reports/proof-coverage-report.md in the certify repo.