[WIP] Hermes.Std #2974

joshlf · 2026-02-03T04:56:30Z

⬇️ Download this PR

Branch

git fetch origin refs/heads/Gb4a4c349671f37aad9e084998afdb7c57d92be43 && git checkout -b pr-Gb4a4c349671f37aad9e084998afdb7c57d92be43 FETCH_HEAD

Checkout

git fetch origin refs/heads/Gb4a4c349671f37aad9e084998afdb7c57d92be43 && git checkout FETCH_HEAD

Cherry Pick

git fetch origin refs/heads/Gb4a4c349671f37aad9e084998afdb7c57d92be43 && git cherry-pick FETCH_HEAD

Pull

git pull origin refs/heads/Gb4a4c349671f37aad9e084998afdb7c57d92be43

Stacked PRs enabled by GHerrit.

gherrit-pr-id: Gb4a4c349671f37aad9e084998afdb7c57d92be43

gemini-code-assist · 2026-02-03T04:56:56Z

Summary of Changes

Hello @joshlf, I'm Gemini Code Assist¹! I'm currently reviewing this pull request and will post my feedback shortly. In the meantime, here's a summary to help you and other reviewers quickly get up to speed!

This pull request establishes a foundational standard library for the Hermes verification framework in Lean, providing essential definitions for type verifiability and memory layout. Concurrently, it overhauls the Rust shadow crate generation process to inject a controlled standard library environment, enabling more precise and robust formal verification of Rust code by routing standard library calls through Hermes-defined shims. These changes are critical for advancing the capabilities and reliability of the Hermes toolchain.

Highlights

Lean Standard Library (Hermes.Std): Introduction of a new Lean module defining core verification concepts like Verifiable types, Layout for memory representation, and platform-specific alignment properties for primitive types.
Rust std and core Shim: Implementation of a custom Rust std and core shim (__hermes_std.rs) within the shadow crate, allowing Hermes to control and model standard library behavior for verification.
Automated Prelude Injection: The shadow crate generation now automatically injects a custom prelude into Rust source files, disabling the default Rust prelude and redirecting std and core imports to the Hermes shim.
Enhanced Argument Parsing: The desugar.rs component now supports parsing instance arguments (e.g., [Layout T]) in addition to regular function arguments, improving the flexibility of Lean specification extraction.
Simplified Proof Stitching: The stitch_user_proofs function in pipeline.rs has been streamlined to always process all Rust source files in the shadow crate, removing the need for a source_file parameter.
Absolute Path Macro Usage: Generated shim code now uses absolute paths for unimplemented! and panic! macros (::std::unimplemented!, ::std::panic!) to avoid conflicts with the custom std re-export.

🧠 New Feature in Public Preview: You can now enable Memory to help Gemini Code Assist learn from your team's feedback. This makes future code reviews more consistent and personalized to your project's style. Click here to enable Memory in your admin console.

Changelog

tools/hermes/src/Hermes.lean
- Added an import statement for the new Hermes.Std module.
tools/hermes/src/desugar.rs
- Updated argument parsing logic to correctly identify and handle instance arguments (e.g., [Layout T]) in addition to traditional function arguments.
tools/hermes/src/include/Std.lean
- Introduced a comprehensive Lean standard library for Hermes, including Verifiable and Layout classes, OfNat instances for various integer types, and platform-specific memory alignment axioms and instances.
tools/hermes/src/include/__hermes_std.rs
- Created a Rust shim file that re-exports the standard library and defines a Lean-annotated ptr::read function, serving as the controlled std and core for the shadow crate.
tools/hermes/src/parser.rs
- Applied minor whitespace formatting adjustments.
tools/hermes/src/pipeline.rs
- Refactored stitch_user_proofs to simplify its interface by removing the source_file parameter and ensuring it always processes all Rust files in the shadow crate's src directory.
- Modified the Lean file generation to import Hermes.Std and related namespaces, and to write the Hermes/Std.lean and Hermes.lean files directly.
- Updated the lean_lib roots in lakefile.lean generation to include Hermes.
tools/hermes/src/shadow.rs
- Implemented a new mechanism to inject the __hermes_std.rs shim into the shadow crate.
- Introduced inject_prelude functionality to modify Rust source files, disabling the implicit prelude and remapping std and core to the Hermes shim.
- Ensured that unimplemented! and panic! macros in generated code use fully qualified paths (::std::unimplemented!, ::std::panic!) to prevent naming conflicts.
tools/hermes/tests/cases/success/shadow_std.rs
- Added a new test case to validate the correct functioning of the std::ptr::read shim with Lean specifications and the new Hermes.Std definitions.

Activity

The pull request introduces a new standard library for Hermes and refactors the shadow crate generation process.
No specific review comments or discussions are available in the provided context.

Using Gemini Code Assist

The full guide for Gemini Code Assist can be found on our documentation page, here are some quick tips.

Invoking Gemini

You can request assistance from Gemini at any point by creating a comment using either /gemini <command> or @gemini-code-assist <command>. Below is a summary of the supported commands on the current page.

Feature	Command	Description
Code Review	`/gemini review`	Performs a code review for the current pull request in its current state.
Pull Request Summary	`/gemini summary`	Provides a summary of the current pull request in its current state.
Comment	@gemini-code-assist	Responds in comments when explicitly tagged, both in pull request comments and review comments.
Help	`/gemini help`	Displays a list of available commands.

Customization

To customize Gemini Code Assist for GitHub experience, repository maintainers can create a configuration file and/or provide a custom code review style guide (such as PEP-8 for Python) by creating and adding files to a .gemini/ folder in the base of the repository. Detailed instructions can be found here.

Limitations & Feedback

Gemini Code Assist may make mistakes. Please leave feedback on any instances where its feedback is incorrect or counter productive. You can react with 👍 and 👎 on @gemini-code-assist comments. If you're interested in giving your feedback about your experience with Gemini Code Assist for Github and other Google products, sign up here.

You can also get AI-powered code generation, chat, as well as code reviews directly in the IDE at no cost with the Gemini Code Assist IDE Extension.

Review the Privacy Notices, Generative AI Prohibited Use Policy, Terms of Service, and learn how to configure Gemini Code Assist in GitHub here. Gemini can make mistakes, so double check it and use code with caution. ↩

gemini-code-assist

Code Review

This pull request introduces a Hermes.Std module for Lean, providing standard definitions for verification like Verifiable, Layout, and memory concepts. This is a significant and positive refactoring that moves hardcoded Lean prelude code into dedicated .lean files, greatly improving modularity and maintainability. The std shadowing mechanism is also updated to support this new structure. The changes are well-implemented, but I have a few minor suggestions for cleanup: a typo fix in a comment, removing a duplicated import, and deleting an unused function.

gemini-code-assist · 2026-02-03T04:58:10Z

tools/hermes/src/desugar.rs

            ensures_clause = Some(ens.trim().to_string());
        } else if signature_args.is_none() && extra_args.is_empty() && ensures_clause.is_none() {
-            // Check if this line looks like signature args.
+            // Check if this file looks like signature args.


There's a small typo in this comment. It should refer to line instead of file, as the check is being performed on the line variable from the loop.

Suggested change

// Check if this file looks like signature args.

// Check if this line looks like signature args.

gemini-code-assist · 2026-02-03T04:58:10Z

tools/hermes/src/shadow.rs

+// Helper to process single source file BEFORE prelude injection
+fn ensure_single_source(root: &Path, source: Option<&Path>) -> Result<()> {
+    if let Some(src) = source {
+        let file_name = src.file_name().context("Invalid source file name")?;
+        let dest = root.join(file_name);
+        process_file_content(src, &dest)?;
+    }
+    Ok(())
+}


This helper function ensure_single_source appears to be unused and can be removed. It might be a leftover from a previous refactoring.

codecov-commenter · 2026-02-03T04:58:46Z

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 92.02%. Comparing base (a5e54ca) to head (2f29def).

Additional details and impacted files

@@                            Coverage Diff                             @@
##           G2e56baadbd39a08c821418704f521a2cdd8d0e1f    #2974   +/-   ##
==========================================================================
  Coverage                                      92.02%   92.02%           
==========================================================================
  Files                                             19       19           
  Lines                                           6029     6029           
==========================================================================
  Hits                                            5548     5548           
  Misses                                           481      481

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

[WIP] Hermes.Std

2f29def

gherrit-pr-id: Gb4a4c349671f37aad9e084998afdb7c57d92be43

This was referenced Feb 3, 2026

[hermes] Initial commit #2968

Open

[WIP] Parser + --allow-sorry #2969

Open

[WIP] Stitching engine #2971

Open

[WIP] Shadow crate + unsafe #2972

Open

[WIP] Invariants #2973

Open

gemini-code-assist bot reviewed Feb 3, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[WIP] Hermes.Std #2974

[WIP] Hermes.Std #2974

joshlf commented Feb 3, 2026 •

edited

Loading

Uh oh!

gemini-code-assist bot commented Feb 3, 2026

Uh oh!

gemini-code-assist bot left a comment

Uh oh!

gemini-code-assist bot Feb 3, 2026

Uh oh!

gemini-code-assist bot Feb 3, 2026

Uh oh!

codecov-commenter commented Feb 3, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

	// Check if this file looks like signature args.
	// Check if this line looks like signature args.

[WIP] Hermes.Std #2974

Are you sure you want to change the base?

[WIP] Hermes.Std #2974

Conversation

joshlf commented Feb 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

gemini-code-assist bot commented Feb 3, 2026

Summary of Changes

Highlights

Footnotes

Uh oh!

gemini-code-assist bot left a comment

Choose a reason for hiding this comment

Code Review

Uh oh!

gemini-code-assist bot Feb 3, 2026

Choose a reason for hiding this comment

Uh oh!

gemini-code-assist bot Feb 3, 2026

Choose a reason for hiding this comment

Uh oh!

codecov-commenter commented Feb 3, 2026

Codecov Report

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

joshlf commented Feb 3, 2026 •

edited

Loading