Skip to content

[WIP] Shadow crate + unsafe #2972

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
joshlf wants to merge 1 commit into
base: G443fc7f8c3623131b48be56a7a16935a9fe8f234
Choose a base branch
from
Open

[WIP] Shadow crate + unsafe #2972

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion tools/hermes/Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,5 +9,5 @@ clap = { version = "4.5.56", features = ["derive"] }
regex = "1.12.2"
walkdir = "2.5.0"
cargo_metadata = "0.18"
syn = { version = "2.0.114", features = ["full", "visit", "extra-traits"] }
syn = { version = "2.0.114", features = ["full", "visit", "visit-mut", "extra-traits"] }
quote = "1.0.43"
1 change: 1 addition & 0 deletions tools/hermes/src/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,4 +17,5 @@ pub mod desugar;
pub mod orchestration;
pub mod parser;
pub mod pipeline;
pub mod shadow;
pub mod translator;
21 changes: 6 additions & 15 deletions tools/hermes/src/parser.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ pub struct ParsedFunction {
pub sig: syn::Signature,
pub spec: Option<String>,
pub proof: Option<String>,
pub is_model: bool,
}

pub struct ExtractedBlocks {
Expand Down Expand Up @@ -53,6 +54,7 @@ impl<'ast> Visit<'ast> for SpecVisitor {
let mut spec_lines = Vec::new();
let mut proof_lines = Vec::new();
let mut current_mode = None; // None, Some("spec"), Some("proof")
let mut is_model = false;

for attr in &node.attrs {
if let Some(doc_str) = parse_doc_attr(attr) {
Expand All @@ -64,11 +66,8 @@ impl<'ast> Visit<'ast> for SpecVisitor {
current_mode = Some("spec");
spec_lines.push(content.to_string());
} else if let Some(content) = trimmed.strip_prefix("@ lean model") {
current_mode = Some("spec"); // Treat model as spec for now? Or maybe distinct?
// The design doc says "model" is for unsafe functions, "spec" for safe.
// For now we treat them somewhat similarly but we might want to distinguish later.
// The user prompt said: "Translate ... functions into rigorous Lean 4 theorems".
// Let's just capture it as spec for now, desugarer can parse the content if needed.
current_mode = Some("spec");
is_model = true;
spec_lines.push(content.to_string());
} else if let Some(content) = trimmed.strip_prefix("@ proof") {
current_mode = Some("proof");
Expand All @@ -95,23 +94,15 @@ impl<'ast> Visit<'ast> for SpecVisitor {
}

let spec = if !spec_lines.is_empty() {
let full_spec = spec_lines.join("\n");
let trimmed_spec = full_spec.trim();
// Strip function name from the beginning of the spec if present?
// Actually, typically `lean spec foo ...` -> logic strips `foo`.
// But here we just capture the raw lines after `@ lean spec`.
// `strip_prefix("@ lean spec")` above leaves the rest of the line.
// e.g. `///@ lean spec foo (x : ...)` -> ` foo (x : ...)`
// We should trim it.
Some(trimmed_spec.to_string())
Some(spec_lines.join("\n").trim().to_string())
} else {
None
};

let proof = if !proof_lines.is_empty() { Some(proof_lines.join("\n")) } else { None };

if spec.is_some() || proof.is_some() {
self.functions.push(ParsedFunction { sig: node.sig.clone(), spec, proof });
self.functions.push(ParsedFunction { sig: node.sig.clone(), spec, proof, is_model });
}

// Continue visiting children (though heavily nested functions are rare/unsupported for specs usually)
Expand Down
79 changes: 51 additions & 28 deletions tools/hermes/src/pipeline.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -101,7 +101,31 @@ pub fn run_pipeline(
fs::remove_file(&llbc_path)?;
}

run_charon(crate_root, &llbc_path, manifest_path.as_deref())?;
// Only pass manifest_path as source_file if it is an .rs file (script)
let source_file = if let Some(path) = &manifest_path {
if path.extension().map_or(false, |e| e == "rs") { Some(path.as_path()) } else { None }
} else {
None
};

println!("Step 1: Creating Shadow Crate...");
let (shadow_crate_root, shadow_source_file) =
crate::shadow::create_shadow_crate(crate_root, source_file)?;

// Remap manifest path to use shadow crate
let shadow_manifest_path = if let Some(shadow_file) = shadow_source_file {
Some(shadow_file)
} else if let Some(path) = &manifest_path {
if let Ok(rel) = path.strip_prefix(crate_root) {
Some(shadow_crate_root.join(rel))
} else {
Some(path.clone())
Copy link
Contributor

@gemini-code-assist gemini-code-assist bot Feb 3, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

high

This else branch seems problematic. If manifest_path is outside crate_root, strip_prefix will fail, and shadow_manifest_path will be set to the original manifest_path. However, run_charon is executed inside the shadow_crate_root. This will likely cause charon to run on the original crate instead of the shadowed one, defeating the purpose of this new mechanism. This case should probably result in an error or be handled differently to ensure the shadowed manifest is always used.

}
} else {
None
};

run_charon(&shadow_crate_root, &llbc_path, shadow_manifest_path.as_deref())?;

if !llbc_path.exists() {
return Err(anyhow!("Charon did not produce expected LLBC file: {:?}", llbc_path));
Expand All @@ -128,25 +152,7 @@ pub fn run_pipeline(
return Err(anyhow!("Aeneas did not produce expected output file: {:?}", generated_camel));
}

// Only pass manifest_path as source_file if it is an .rs file (script)
let source_file = if let Some(path) = &manifest_path {
if path.extension().map_or(false, |e| e == "rs") {
Some(path.as_path())
} else {
None
}
} else {
None
};

stitch_user_proofs(
&crate_root,
&crate_name_snake,
&camel_name,
dest,
source_file,
sorry_mode,
)?;
stitch_user_proofs(&crate_root, &crate_name_snake, &camel_name, dest, source_file, sorry_mode)?;

println!("Step 4: Verifying...");
write_lakefile(dest, &crate_name_snake, &camel_name, aeneas_path, sorry_mode)?;
Expand Down Expand Up @@ -202,6 +208,18 @@ fn generate_lean_file(
content.push_str("open Aeneas Aeneas.Std Result Error\n\n");
content.push_str(&format!("namespace {}\n\n", namespace_name));

// Inject OfNat instances to support numeric literals in specs (e.g. `x > 0`)
// We use wrapping construction (BitVec.ofNat) to avoid needing in-bounds proofs.
content.push_str(
"
instance : OfNat U32 n where ofNat := UScalar.mk (BitVec.ofNat 32 n)
instance : OfNat I32 n where ofNat := IScalar.mk (BitVec.ofNat 32 n)
instance : OfNat Usize n where ofNat := UScalar.mk (BitVec.ofNat System.Platform.numBits n)
instance : OfNat Isize n where ofNat := IScalar.mk (BitVec.ofNat System.Platform.numBits n)

",
);

for func in functions {
let spec_content = match &func.spec {
Some(s) => s,
Expand All @@ -210,10 +228,11 @@ fn generate_lean_file(

let fn_name = func.sig.ident.to_string();

let proof_body = match (&func.proof, sorry_mode) {
(Some(proof), _) => proof.as_str(),
(None, Sorry::AllowSorry) => "sorry",
(None, Sorry::RejectSorry) => anyhow::bail!(
let proof_body = match (&func.proof, sorry_mode, func.is_model) {
(Some(proof), _, _) => proof.as_str(),
(None, _, true) => "sorry", // Models are implicitly trusted/admitted
(None, Sorry::AllowSorry, _) => "sorry",
(None, Sorry::RejectSorry, _) => anyhow::bail!(
"Missing proof for function '{}'. Use --allow-sorry to fallback to sorry.",
fn_name
),
Expand Down Expand Up @@ -247,12 +266,16 @@ fn generate_lean_file(

let signature = signature_parts.join(" ");

content.push_str(&format!("theorem {}_spec {}\n", fn_name, signature));
let decl_type = if func.is_model && func.proof.is_none() { "axiom" } else { "theorem" };

content.push_str(&format!("{} {}_spec {}\n", decl_type, fn_name, signature));
content.push_str(&format!(" : {}\n", desugared.body));

content.push_str(" :=\n");
content.push_str(" by\n");
content.push_str(proof_body);
if decl_type == "theorem" {
content.push_str(" :=\n");
content.push_str(" by\n");
content.push_str(proof_body);
}
content.push_str("\n\n");
}

Expand Down
Loading
Loading