Hermes: `cargo hermes verify` fails with `-split-files` due to file structure and import issues

[AlephNotation]

Summary

cargo hermes verify doesn't work end-to-end when Aeneas runs with -split-files. Several issues in pipeline.rs and orchestration.rs prevent the generated Lean project from building.

Reproduction

Create a simple annotated Rust file:

///@ lean spec is_temporally_valid (exp : U64) (nbf : Option U64) (now : U64)
///@ ensures |ret| (ret = true → now.val < exp.val)
///@ proof
///@   sorry
pub fn is_temporally_valid(exp: u64, nbf: Option<u64>, now: u64) -> bool {
    if now >= exp { return false; }
    if let Some(t) = nbf { if now < t { return false; } }
    true
}

Run:

cargo hermes verify --manifest-path test.rs --dest output \
  --aeneas-path "$AENEAS_PATH/backends/lean" --allow-sorry

Issues Found

1. Missing -gen-lib-entry flag

File: orchestration.rs
Aeneas with -split-files needs -gen-lib-entry to generate the root CamelName.lean entry file. Without it, the pipeline can't find the expected output.

2. Split files not moved into subdirectory

File: pipeline.rs
Aeneas outputs Types.lean, Funs.lean flat in the dest directory, but the generated entry file imports CamelName.Funs — expecting CamelName/Funs.lean. Files need to be moved into a CamelName/ subdirectory.

3. FunsExternal.lean uses snake_case imports

File: pipeline.rs, generate_lean_file()
Writes import {namespace_name}.Types (e.g. import temporal_validity.Types) but should use import {import_name}.Types (e.g. import TemporalValidity.Types). The namespace_name variable is snake_case; import_name is the CamelCase version.

4. Unconditional Hermes.Std imports break simple cases

File: pipeline.rs, generate_lean_file()
UserProofs.lean always opens Hermes.Std.Memory, Hermes.Std.Platform, and {namespace}.hermes_std.ptr even when no models or invariants exist. This causes Lean errors for non-existent namespaces.

5. hermes_std functions leak into UserProofs.lean

The injected hermes_std::ptr::read model gets stitched into UserProofs.lean with specs that reference Verifiable, ConstPtr, Memory.is_initialized — types that don't exist unless Hermes.Std is imported. These internal functions are already handled by the Aeneas template.

6. Proof indentation lost

Proof body from ///@ annotations loses its whitespace during extraction, producing malformed Lean.

Proposed Fix

See PR #3065 which addresses all of these.

[joshlf]

Hermes has been reimplemented from scratch on the hermes branch. I believe all of these have been resolved there, but feel free to re-open if not.