From 0c4aad94ef247dfe043c5e7464a0e64ef8a16b69 Mon Sep 17 00:00:00 2001 From: Joshua Liebow-Feeser Date: Wed, 4 Feb 2026 01:57:18 +0000 Subject: [PATCH] [WIP] Model unsafe functions as noncomputable gherrit-pr-id: G8b674511787c67f5fdb20d28e10d9387316037ae --- tools/hermes/src/desugar.rs | 26 +- tools/hermes/src/include/__hermes_std.rs | 2 +- tools/hermes/src/orchestration.rs | 16 +- tools/hermes/src/pipeline.rs | 242 ++++++++++++--- tools/hermes/src/shadow.rs | 281 +++++++++++------- .../tests/cases/failure/model_mut_ref.rs | 9 + 6 files changed, 418 insertions(+), 158 deletions(-) create mode 100644 tools/hermes/tests/cases/failure/model_mut_ref.rs diff --git a/tools/hermes/src/desugar.rs b/tools/hermes/src/desugar.rs index 16d84e7d37..8782d53e4f 100644 --- a/tools/hermes/src/desugar.rs +++ b/tools/hermes/src/desugar.rs @@ -6,6 +6,8 @@ pub struct DesugaredSpec { pub signature_args: Option, pub extra_args: Vec, // e.g., (h_safe : ...) pub body: String, + pub predicate: Option, + pub binders: Vec, } pub fn desugar_spec( @@ -49,16 +51,16 @@ pub fn desugar_spec( // Construct body // If ensures |ret, x_final| ... - let body = if let Some(ens) = ensures_clause { + let body = if let Some(ens) = &ensures_clause { // Parse binders |...| - let (binders, logic) = parse_binders(&ens)?; + let (binders, logic) = parse_binders(ens)?; let user_logic = if !logic_lines.is_empty() { // Maybe prepend logic lines? // Actually currently valid syntax is usually `ensures |...| logic`. // `logic_lines` might be empty or continuations. // Let's assume `logic` from ensures line + `logic_lines` joined. let mut full = logic; - for l in logic_lines { + for l in &logic_lines { full.push_str("\n "); full.push_str(l); } @@ -81,10 +83,24 @@ pub fn desugar_spec( } }; - Ok(DesugaredSpec { signature_args, extra_args, body }) + let (predicate, binders) = if let Some(ens) = &ensures_clause { + let (binders, logic) = parse_binders(ens)?; + let mut full = logic; + if !logic_lines.is_empty() { + for l in &logic_lines { + full.push_str("\n "); + full.push_str(l); + } + } + (Some(full), binders) + } else { + (None, Vec::new()) + }; + + Ok(DesugaredSpec { signature_args, extra_args, body, predicate, binders }) } -fn parse_binders(ensures_content: &str) -> Result<(Vec, String)> { +pub fn parse_binders(ensures_content: &str) -> Result<(Vec, String)> { // |ret, x_final| logic if let Some(start) = ensures_content.find('|') && let Some(end) = ensures_content[start + 1..].find('|') diff --git a/tools/hermes/src/include/__hermes_std.rs b/tools/hermes/src/include/__hermes_std.rs index 1aab53192a..b2f4279d72 100644 --- a/tools/hermes/src/include/__hermes_std.rs +++ b/tools/hermes/src/include/__hermes_std.rs @@ -27,7 +27,7 @@ pub mod ptr { ///@ requires h_init : Memory.is_initialized src ///@ ensures |ret| Verifiable.is_valid ret pub unsafe fn read(src: *const T) -> T { - unsafe { ::std::ptr::read(src) } + loop {} } } diff --git a/tools/hermes/src/orchestration.rs b/tools/hermes/src/orchestration.rs index d7cb107027..dbb003324b 100644 --- a/tools/hermes/src/orchestration.rs +++ b/tools/hermes/src/orchestration.rs @@ -16,7 +16,13 @@ use anyhow::{Context, Result, anyhow}; /// * `crate_root` - Path to the root of the crate to analyze. /// * `dest_file` - Destination path for the LLBC file (e.g. `.../crate.llbc`). /// * `manifest_path` - Optional path to a specific Cargo.toml or script file. -pub fn run_charon(crate_root: &Path, dest_file: &Path, manifest_path: Option<&Path>) -> Result<()> { +/// * `opaque_funcs` - List of fully qualified function names to mark as opaque. +pub fn run_charon( + crate_root: &Path, + dest_file: &Path, + manifest_path: Option<&Path>, + opaque_funcs: &[String], +) -> Result<()> { let crate_root = crate_root.to_str().unwrap(); let dest_file = dest_file.to_str().unwrap(); @@ -34,6 +40,11 @@ pub fn run_charon(crate_root: &Path, dest_file: &Path, manifest_path: Option<&Pa // Charon args first args(&mut cmd, &["--dest-file", dest_file, "--preset", "aeneas", "--error-on-warnings"]); + for func in opaque_funcs { + cmd.arg("--opaque"); + cmd.arg(func); + } + if let Some(path) = manifest_path { cmd.arg("--"); if path.extension().is_some_and(|e| e == "rs") { @@ -50,7 +61,7 @@ pub fn run_charon(crate_root: &Path, dest_file: &Path, manifest_path: Option<&Pa Ok(()) } -const ALL_AENEAS_BACKENDS: &str = "BorrowCheck,Builtin,Contexts,Deps,Errors,Extract,FunsAnalysis,Interp,InterpAbs,InterpBorrows,InterpExpansion,InterpExpressions,InterpJoin,InterpLoops,InterpLoopsFixedPoint,InterpMatchCtxs,InterpPaths,InterpProjectors,InterpReduceCollapse,InterpStatements,Invariants,MainLogger,PrePasses,PureMicroPasses,PureMicroPasses.simplify_aggregates_unchanged_fields,PureTypeCheck,PureUtils,RegionsHierarchy,ReorderDecls,SCC,SymbolicToPure,SymbolicToPureAbs,SymbolicToPureExpressions,SymbolicToPureTypes,SymbolicToPureValues,Translate,TypesAnalysis"; +const _ALL_AENEAS_BACKENDS: &str = "BorrowCheck,Builtin,Contexts,Deps,Errors,Extract,FunsAnalysis,Interp,InterpAbs,InterpBorrows,InterpExpansion,InterpExpressions,InterpJoin,InterpLoops,InterpLoopsFixedPoint,InterpMatchCtxs,InterpPaths,InterpProjectors,InterpReduceCollapse,InterpStatements,Invariants,MainLogger,PrePasses,PureMicroPasses,PureMicroPasses.simplify_aggregates_unchanged_fields,PureTypeCheck,PureUtils,RegionsHierarchy,ReorderDecls,SCC,SymbolicToPure,SymbolicToPureAbs,SymbolicToPureExpressions,SymbolicToPureTypes,SymbolicToPureValues,Translate,TypesAnalysis"; /// Runs the Aeneas tool to translate LLBC files into Lean code. /// @@ -77,6 +88,7 @@ pub fn run_aeneas(llbc_path: &Path, dest: &Path) -> Result<()> { llbc_path, "-dest", dest, + "-split-files", ], ); let status = cmd.status().context("Failed to execute aeneas. Ensure it is in your PATH.")?; diff --git a/tools/hermes/src/pipeline.rs b/tools/hermes/src/pipeline.rs index 1eb13b1849..93fa4032dd 100644 --- a/tools/hermes/src/pipeline.rs +++ b/tools/hermes/src/pipeline.rs @@ -109,7 +109,7 @@ pub fn run_pipeline( }; log::info!("Step 1: Creating Shadow Crate..."); - let (shadow_crate_root, shadow_source_file) = + let (shadow_crate_root, shadow_source_file, models) = crate::shadow::create_shadow_crate(crate_root, source_file)?; // Remap manifest path to use shadow crate @@ -125,7 +125,11 @@ pub fn run_pipeline( None }; - run_charon(&shadow_crate_root, &llbc_path, shadow_manifest_path.as_deref())?; + // Prepend crate name to models + let opaque_funcs: Vec = + models.iter().map(|m| format!("{}::{}", crate_name_snake, m)).collect(); + + run_charon(&shadow_crate_root, &llbc_path, shadow_manifest_path.as_deref(), &opaque_funcs)?; if !llbc_path.exists() { return Err(anyhow!("Charon did not produce expected LLBC file: {:?}", llbc_path)); @@ -203,24 +207,46 @@ fn generate_lean_file( structs: &[crate::parser::ParsedStruct], sorry_mode: Sorry, ) -> Result<()> { - let mut content = String::new(); - content.push_str(&format!( + let mut user_proofs_content = String::new(); + let mut funs_external_content = String::new(); + + let common_imports = format!( "import {} import Aeneas import Hermes.Std open Aeneas Aeneas.Std Result Error open Hermes.Std open Hermes.Std.Memory -open Hermes.Std.Memory open Hermes.Std.Platform open {}.hermes_std.ptr set_option linter.unusedVariables false -namespace {} - ", - import_name, namespace_name, namespace_name - )); + import_name, namespace_name + ); + + // FunsExternal needs to import Types? Yes, usually via `import_name` (e.g. ShadowModel or GenericId). + // Actually, `import_name` usually imports `Funs` which imports `Types`. + // But `Funs` imports `FunsExternal`. Cycle! + // `FunsExternal` should only import `Types`. + // We assume `import {import_name}` imports the top-level generic_id.lean which imports Funs/Types? + // No, Aeneas structure: + // {Crate}.lean imports Funs, Types. + // Funs imports Types, FunsExternal. + // So FunsExternal should import Types explicitly if needed. + // `import_name` usually refers to the crate which might not verify yet if we are circular. + // Aeneas typically generates module structure: `namespace.Types`, `namespace.Funs`. + // We should import `{namespace_name}.Types`. + + funs_external_content.push_str(&format!("import {}.Types\n", namespace_name)); + funs_external_content.push_str("import Aeneas\n"); + funs_external_content.push_str("import Hermes.Std\n"); + funs_external_content.push_str("open Aeneas Aeneas.Std Result Error\n"); + funs_external_content.push_str("open Hermes.Std\n"); + funs_external_content.push_str(&format!("\nnamespace {}\n\n", namespace_name)); + + user_proofs_content.push_str(&common_imports); + user_proofs_content.push_str(&format!("namespace {}\n\n", namespace_name)); // Write Hermes/Std.lean let hermes_std_path = dest.join("Hermes"); @@ -228,7 +254,8 @@ namespace {} fs::write(hermes_std_path.join("Std.lean"), include_str!("include/Std.lean"))?; fs::write(dest.join("Hermes.lean"), include_str!("Hermes.lean"))?; - // Struct Instances + // Struct Instances (UserProofs) + // ... (keep struct logic) // Dedup structs just in case let mut unique_structs = Vec::new(); let mut seen_structs = std::collections::HashSet::new(); @@ -258,7 +285,6 @@ namespace {} } } - // Format: instance {T} [Verifiable T] : Verifiable (Wrapper T) where let type_str = if type_args.is_empty() { name.to_string() } else { @@ -269,10 +295,11 @@ namespace {} "instance {}{} : Verifiable {} where", generic_params, generic_constraints, type_str ); - content.push_str(&header); - content.push_str(&format!("\n is_valid self := {}\n\n", invariant)); + user_proofs_content.push_str(&header); + user_proofs_content.push_str(&format!("\n is_valid self := {}\n\n", invariant)); } + // Process Functions for func in functions { let spec_content = match &func.spec { Some(s) => s, @@ -280,22 +307,17 @@ namespace {} }; let fn_name = func.sig.ident.to_string(); + let inputs: Vec = func.sig.inputs.iter().cloned().collect(); + let is_stateful = SignatureTranslator::detect_statefulness(&inputs); - 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.", + if func.is_model && is_stateful { + anyhow::bail!( + "Function '{}' is marked as a model but has mutable references. This is not supported.", fn_name - ), - }; + ); + } let generics_context = SignatureTranslator::translate_generics(&func.sig.generics); - - let inputs: Vec = func.sig.inputs.iter().cloned().collect(); - let is_stateful = SignatureTranslator::detect_statefulness(&inputs); - let desugared = match desugar_spec(spec_content, &fn_name, &inputs, is_stateful) { Ok(d) => d, Err(e) => { @@ -304,53 +326,177 @@ namespace {} } }; - let mut signature_parts = Vec::new(); + let mut signature_args_full = Vec::new(); if !generics_context.is_empty() { - signature_parts.push(generics_context); + signature_args_full.push(generics_context.clone()); + } + if let Some(args) = &desugared.signature_args { + signature_args_full.push(args.clone()); } - if let Some(args) = desugared.signature_args { - signature_parts.push(args); + if func.is_model { + // Generate External Definition + // 1. Spec Predicate + // def foo_spec (args...) (ret...) : Prop := ... + // The desugared.predicate contains the logic. + // We need to construct the arguments for the spec. + // desugared.signature_args has (x : T). destuared.binders has names of rets. + // We need types for rets? + // desugar doesn't infer types. + // But usually spec is written like: `ensures |ret| ...` + // In Lean, we can rely on inference if we use `exists ret, ...` + // But for `def foo_spec args ret : Prop`, we need ret's Type. + // Either we parse it from the signature (RetType) or we trust user provided it? + // User provided `ensures |ret| ...`. No type info. + // So `foo_spec` signature is hard to generate fully typed without more info. + // However, we can define `foo_spec` as: + // `def foo_spec args ret := logic` + // relying on Lean to infer types from the logic body? + // Or we just inline it in the `exists`. + // + // Let's rely on the `desugar.body` which is `exists ret, ...`. + // Wait, `desugar.body` is designed for theorem statement: `foo_fwd ... = ...`. + // It is NOT the predicate `P /\ Q`. + // `desugared.predicate` IS the logic `P /\ Q`. + // + // Let's generate: + // `noncomputable def foo (args...) : Result RetType :=` + // ` if h : exists ret, (predicate_substituted) then` + // + // Problem: `predicate` uses binder names. + // We need to say `exists ret, (logic with ret)`. + // + // `desugared.predicate` is `Some("logic")`. + // `desugared.binders` is `["ret"]`. + // + // Content: + // noncomputable def {fn_name} {signature_args} : Result {RetType} := + // if h : exists {binders}, {predicate} then + // let v := Classical.choose h + // Result.ok v + // else + // Result.fail Error.panic + // + // We need `RetType`. `ParsedFunction` has `sig` which has `output`. + // We can translate `output` to Lean type? + // `translator.rs` doesn't have type translator yet. + // BUT `desugar` might have extracted signature args? No. + // `parsed_function` has `sig`. + // + // Use Aeneas naming? + // Aeneas usually generates `def foo ... : Result T`. + // If we redeclare it, we must match exactly. + // + // Alternative: + // Reuse the `desugared.body` which was: `exists ret, foo_fwd ... = Result.ok ret /\ logic`. + // This body asserts that the function matches the logic. + // It doesn't help us DEFINE the function. + // + // We genuinely need the return type to write the signature of `noncomputable def`. + // + // Hack: Can we avoid explicit type? + // `noncomputable def foo ... := ...` (infer return type?) + // `Result.ok (Classical.choose h)` -> implies Result T. + // Lean might infer it? + // + // Let's try omitting return type if possible? + // `noncomputable def foo {signature_args} :=` + // + // Need to ensure `signature_args` covers all args. + // + // AND `desugared.binders`: if multiple (tuple), `Classical.choose h` returns a tuple. + // + // Let's construct it. + + let sig_str = signature_args_full.join(" "); + // Note: `signature_args` usually is `(x : U32) ...`. + + let pred = desugared.predicate.as_deref().unwrap_or("True"); + let binders_str = desugared.binders.join(" "); // "ret" or "ret1 ret2" + + // "exists ret, P" + let exists_clause = if desugared.binders.is_empty() { + pred.to_string() // Just logic? + } else { + format!("exists {}, {}", binders_str, pred) + }; + + funs_external_content + .push_str(&format!("noncomputable def {} {} :=\n", fn_name, sig_str)); + funs_external_content.push_str(&format!(" if h : {} then\n", exists_clause)); + if desugared.binders.is_empty() { + funs_external_content.push_str(" Result.ok ()\n"); + } else { + funs_external_content.push_str(" Result.ok (Classical.choose h)\n"); + } + funs_external_content.push_str(" else\n Result.fail Error.panic\n\n"); } - // INJECT ARGUMENT VALIDITY CHECKS - // For each arg `x : T`, inject `(h_x : Verifiable.is_valid x)` - // We need to parse inputs to get names. + // Spec Generation (Common for Model and Verified) + // Standard Verified Function or Model Spec + let proof_body = match &func.proof { + Some(p) => p.as_str(), + None => match sorry_mode { + Sorry::AllowSorry => "sorry", + Sorry::RejectSorry => { + if func.is_model { + "axiom" + } else { + anyhow::bail!("Missing proof for '{}'.", fn_name) + } + } + }, + }; + + // Signature parts for UserProofs + let mut sig_parts = signature_args_full.clone(); + + // Inject Argument Validity Checks for arg in &inputs { if let syn::FnArg::Typed(pat_type) = arg && let syn::Pat::Ident(pat_ident) = &*pat_type.pat { let name = &pat_ident.ident; - // We assume the type is verifiable. - // The signature args in `desugared.signature_args` already listed them as `(x : T)`. - // We just append validity hypotheses. - // Note: This relies on `x` being available in scope, which it is in the signature. - signature_parts.push(format!("(h_{}_valid : Verifiable.is_valid {})", name, name)); + sig_parts.push(format!("(h_{}_valid : Verifiable.is_valid {})", name, name)); } } - for req in desugared.extra_args { - signature_parts.push(req); + for req in &desugared.extra_args { + sig_parts.push(req.clone()); } - let signature = signature_parts.join(" "); + let signature = sig_parts.join(" "); let decl_type = if func.is_model && func.proof.is_none() { "axiom" } else { "theorem" }; + // If proof_body is "axiom", decl_type is axiom. + // Actually logic above: + // if model and no proof -> "axiom" body? No, body is empty for axiom. - content.push_str(&format!("{} {}_spec {}\n", decl_type, fn_name, signature)); - content.push_str(&format!(" : {}\n", desugared.body)); + user_proofs_content.push_str(&format!("{} {}_spec {}\n", decl_type, fn_name, signature)); + user_proofs_content.push_str(&format!(" : {}\n", desugared.body)); if decl_type == "theorem" { - content.push_str(" :=\n"); - content.push_str(" by\n"); - content.push_str(proof_body); + user_proofs_content.push_str(" :=\n"); + user_proofs_content.push_str(" by\n"); + user_proofs_content.push_str(proof_body); } - content.push_str("\n\n"); + user_proofs_content.push_str("\n\n"); } - content.push_str(&format!("end {}\n", namespace_name)); + user_proofs_content.push_str(&format!("end {}\n", namespace_name)); + funs_external_content.push_str(&format!("end {}\n", namespace_name)); + + fs::write(dest.join("UserProofs.lean"), user_proofs_content)?; - fs::write(dest.join("UserProofs.lean"), content).map_err(Into::into) + // Only write FunsExternal if we have content? + // Aeneas generates Template if it misses it. + // If we write it, Aeneas should be happy. + // Even if empty? + if !funs_external_content.is_empty() { + fs::write(dest.join("FunsExternal.lean"), funs_external_content)?; + } + + Ok(()) } fn write_lakefile( diff --git a/tools/hermes/src/shadow.rs b/tools/hermes/src/shadow.rs index 5877249818..5eeb0071bb 100644 --- a/tools/hermes/src/shadow.rs +++ b/tools/hermes/src/shadow.rs @@ -19,13 +19,13 @@ use walkdir::WalkDir; pub fn create_shadow_crate( original_root: &Path, source_file: Option<&Path>, -) -> Result<(PathBuf, Option)> { +) -> Result<(PathBuf, Option, Vec)> { // 1. Destination: target/hermes_shadow let shadow_root = original_root.join("target").join("hermes_shadow"); if shadow_root.exists() { - fs::remove_dir_all(&shadow_root).context("Failed to clean shadow directory")?; + fs::remove_dir_all(&shadow_root)?; } - fs::create_dir_all(&shadow_root).context("Failed to create shadow directory")?; + fs::create_dir_all(&shadow_root)?; // 2. Recursive Copy (only if not a single-file script, OR generally?) // If it's a script, original_root might be unrelated. @@ -71,7 +71,7 @@ pub fn create_shadow_crate( fs::write(&shim_path, SHIM_CONTENT).context("Failed to write shadow std shim")?; // 4. Sanitization - sanitize_crate(&shadow_root)?; + let mut models = sanitize_crate(&shadow_root)?; // 5. Handle Single Source File (Write it now so we can inject prelude) let shadow_source_file = if let Some(source) = source_file { @@ -82,7 +82,8 @@ pub fn create_shadow_crate( fs::create_dir_all(parent)?; } // Sanitize and write - process_file_content(source, &dest_path)?; + let file_models = process_file_content(source, &dest_path)?; + models.extend(file_models); Some(dest_path) } else { None @@ -109,7 +110,7 @@ pub fn create_shadow_crate( } // Return - Ok((shadow_root, shadow_source_file)) + Ok((shadow_root, shadow_source_file, models)) } const SHIM_CONTENT: &str = include_str!("include/__hermes_std.rs"); @@ -127,8 +128,6 @@ fn inject_prelude(path: &Path) -> Result<()> { let mut ast = syn::parse_file(&content)?; // 1. Disable the built-in Rust prelude (Inner Attribute) - // We append to existing attributes or prepend? Order matters if there are other attributes that depend on prelude? - // Usually no_implicit_prelude is fine anywhere in headers. ast.attrs.push(parse_quote!(#![no_implicit_prelude])); // 2. Prepare Injection Items @@ -152,8 +151,17 @@ fn inject_prelude(path: &Path) -> Result<()> { #[allow(unused_imports)] use std::prelude::rust_2021::*; ), + // mod charon { pub use charon_macros::opaque; } + // We need `charon_macros` to exist or be faked. + // Actually, since we rewrite the crate, we can just define a dummy `opaque` attribute logic? + // Rustc allows custom attributes if they are mapped to a tool or via `register_tool` (nightly). + // For stable, we might need a dummy macro or just `allow` it? + // But `#[charon::opaque]` looks like a path attribute. + // Let's define: `pub mod charon { pub use crate::hermes_std::opaque; }` + // and in `hermes_std` define `pub use ...`? + // Simpler: define `mod charon` right here which exports a dummy `opaque` attribute macro? + // Attributes must be macros. ]; - // 3. Insert at the beginning of items (AFTER inner attributes) ast.items.splice(0..0, prelude_items); @@ -162,110 +170,145 @@ fn inject_prelude(path: &Path) -> Result<()> { Ok(()) } -fn process_file_content(src: &Path, dest: &Path) -> Result<()> { +fn process_file_content(src: &Path, dest: &Path) -> Result> { let content = fs::read_to_string(src)?; let mut ast = syn::parse_file(&content)?; - let mut visitor = ShadowVisitor; + let mut visitor = ShadowVisitor::new(); visitor.visit_file_mut(&mut ast); let new_content = quote!(#ast).to_string(); fs::write(dest, new_content)?; - Ok(()) + Ok(visitor.models) } -fn sanitize_crate(root: &Path) -> Result<()> { +fn sanitize_crate(root: &Path) -> Result> { let src_dir = root.join("src"); + let mut all_models = Vec::new(); if !src_dir.exists() { - return Ok(()); + return Ok(all_models); } for entry in WalkDir::new(&src_dir) { let entry = entry?; if entry.file_type().is_file() && entry.path().extension().is_some_and(|e| e == "rs") { - process_file(entry.path())?; + let relative = entry.path().strip_prefix(&src_dir)?; + // Map file path to module path (simplistic: foo/bar.rs -> foo::bar) + // Note: ShadowVisitor tracks `current_path` relative to the file. + // We need to prepend the module path derived from file structure? + // Wait, ShadowVisitor `current_path` is empty at file root. + // But if we are processing `src/foo/bar.rs`, the functions in it are in `foo::bar`. + // `ShadowVisitor` doesn't know this external context unless we tell it. + // OR we fix up the returned models. + // `visitor.models` will contain e.g. `my_func` or `inner::my_func`. + // We need to prepend `foo::bar`. + + // Logic for module path: + let components: Vec<_> = relative + .with_extension("") + .iter() + .map(|s| s.to_string_lossy().into_owned()) + .collect(); + // If filename is `mod.rs` or `lib.rs` or `main.rs`, handle accordingly. + let mut mod_path = Vec::new(); + for (i, comp) in components.iter().enumerate() { + if i == components.len() - 1 && (comp == "mod" || comp == "lib" || comp == "main") { + continue; + } + mod_path.push(comp.clone()); + } + + let file_models = process_file(entry.path())?; + for m in file_models { + let full = + if mod_path.is_empty() { m } else { format!("{}::{}", mod_path.join("::"), m) }; + all_models.push(full); + } } } - Ok(()) + Ok(all_models) } -fn process_file(path: &Path) -> Result<()> { +fn process_file(path: &Path) -> Result> { let content = fs::read_to_string(path)?; - // If parse fails, we can't extract/sanitize. Fail loudly so user knows. - // Or we could warn and skip? For verification, we want strictness. let mut ast = syn::parse_file(&content)?; - let mut visitor = ShadowVisitor; + let mut visitor = ShadowVisitor::new(); visitor.visit_file_mut(&mut ast); let new_content = quote!(#ast).to_string(); fs::write(path, new_content)?; - Ok(()) + Ok(visitor.models) } -struct ShadowVisitor; +struct ShadowVisitor { + current_path: Vec, + models: Vec, +} + +impl ShadowVisitor { + fn new() -> Self { + Self { current_path: Vec::new(), models: Vec::new() } + } +} impl VisitMut for ShadowVisitor { + fn visit_item_mod_mut(&mut self, i: &mut syn::ItemMod) { + self.current_path.push(i.ident.to_string()); + syn::visit_mut::visit_item_mod_mut(self, i); + self.current_path.pop(); + } + fn visit_item_fn_mut(&mut self, node: &mut ItemFn) { - let (is_model, model_requires) = parse_model_specs(&node.attrs); + let (is_model, _model_requires) = parse_model_specs(&node.attrs); + + if is_model { + // Collect model name + let mut full_path = self.current_path.clone(); + full_path.push(node.sig.ident.to_string()); + self.models.push(full_path.join("::")); + + // Case A: Model Strategy + // 1. Remove unsafe (if present) + node.sig.unsafety = None; + + // 2. Replace body with loop {} (Diverge) + let body_content = quote! { + { + loop {} + } + }; + + let block: syn::Block = syn::parse2(body_content).expect("Failed to parse loop body"); + *node.block = block; + + // Append #[allow(unused_variables)] if not present + let has_allow_unused = node.attrs.iter().any(|attr| { + if attr.path().is_ident("allow") { + if let syn::Meta::List(list) = &attr.meta { + return list.tokens.to_string().contains("unused_variables"); + } + } + false + }); + + if !has_allow_unused { + node.attrs.push(parse_quote!(#[allow(unused_variables)])); + } + return; + } - // We only care about `unsafe fn` + // Pre-existing logic for unwrapping unsafe functions that are NOT models if node.sig.unsafety.is_some() { - if is_model { - // Case A: Model Strategy - // 1. Remove unsafe - node.sig.unsafety = None; - - // 2. Inject Shim - let preconditions = if model_requires.is_empty() { - quote!(true) - } else { - let combined = model_requires.join(") && ("); - let combined_str = format!("{}", combined); - // Parse as Expr to ensure validity and proper token nesting - let expr = syn::parse_str::(&combined_str) - .unwrap_or_else(|_| parse_quote!(true)); - quote!(#expr) - }; - - let body_content = quote! { - { - if #preconditions { - // TODO: If the preconditions are met, we still - // panic. That means that any model we provide will - // be wrong (ie, it will claim that the function - // returns successfully, when in fact it panics). - // This will allow Lean to infer a contradiction, - // allowing any user's proof to be accepted - // regardless of its correctness. - ::std::unimplemented!("Safe Shim") - } else { - ::std::panic!("Contract Violated") - } - } - }; - - // Replace body - if let Ok(block) = syn::parse2(body_content) { - node.block = block; - } + // Case B: Unwrap Strategy + // 1. Remove unsafe + node.sig.unsafety = None; - // Append #[allow(unused_variables)] to suppress warnings/errors - // since the new body doesn't use any of its arguments. It's - // important that we add it at the end to override any - // preceding `#[warn(unused_variables)]` (or `deny`). - node.attrs.push(parse_quote!(#[allow(unused_variables)])); - } else { - // Case B: Unwrap Strategy - // 1. Remove unsafe - node.sig.unsafety = None; - - // 2. Recurse into body to unwrap internal unsafe blocks - syn::visit_mut::visit_item_fn_mut(self, node); - } + // 2. Recurse into body to unwrap internal unsafe blocks + syn::visit_mut::visit_item_fn_mut(self, node); } else { - // Safe function: just recurse - syn::visit_mut::visit_item_fn_mut(self, node); + // Safe function not model: just recurse + syn::visit_mut::visit_item_fn_mut(self, node); } } @@ -292,10 +335,18 @@ fn parse_model_specs(attrs: &[Attribute]) -> (bool, Vec) { let mut is_model = false; let mut requires = Vec::new(); + // Debugging loop + /* + for attr in attrs { + if attr.path().is_ident("doc") { + println!("Found doc attr: {:?}", attr); + } + } + */ + for trimmed in crate::docs::iter_hermes_lines(attrs) { if let Some(_content) = crate::docs::parse_hermes_tag(&trimmed, "lean model") { is_model = true; - log::debug!("Found model marker!"); } if let Some(content) = crate::docs::parse_hermes_tag(&trimmed, "requires") { @@ -316,7 +367,7 @@ mod tests { fn transform(code: &str) -> String { let mut ast = syn::parse_file(code).expect("Failed to parse input"); - let mut visitor = ShadowVisitor; + let mut visitor = ShadowVisitor::new(); visitor.visit_file_mut(&mut ast); quote!(#ast).to_string() } @@ -336,14 +387,19 @@ mod tests { #[test] fn test_leaf_node_basic() { let input = r#" - ///@ lean model foo ensures |ret| ret = 42 - unsafe fn foo() -> i32 { unsafe { *ptr } } + ///@ lean model foo + ///@ ensures |ret| ret = 42 + #[allow(unused_variables)] + fn foo() -> i32 { + unsafe { 0 } + } "#; let expected = r#" - #[doc = "@ lean model foo ensures |ret| ret = 42"] + #[doc = "@ lean model foo"] + #[doc = "@ ensures |ret| ret = 42"] #[allow(unused_variables)] fn foo() -> i32 { - if true { ::std::unimplemented!("Safe Shim") } else { ::std::panic!("Contract Violated") } + loop {} } "#; assert_normalized_eq(&transform(input), expected); @@ -354,14 +410,17 @@ mod tests { let input = r#" ///@ lean model safe_div(a b : u32) ///@ requires b > 0 - unsafe fn safe_div(a: u32, b: u32) -> u32 { 0 } + #[allow(unused_variables)] + fn safe_div(a: u32, b: u32) -> u32 { + unsafe { a / b } + } "#; let expected = r#" #[doc = "@ lean model safe_div(a b : u32)"] #[doc = "@ requires b > 0"] #[allow(unused_variables)] fn safe_div(a: u32, b: u32) -> u32 { - if b > 0 { ::std::unimplemented!("Safe Shim") } else { ::std::panic!("Contract Violated") } + loop {} } "#; assert_normalized_eq(&transform(input), expected); @@ -371,14 +430,17 @@ mod tests { fn test_raw_pointer_signatures() { let input = r#" ///@ lean model read(ptr : Type) ... - unsafe fn read(ptr: *const u32) -> u32 { *ptr } + #[allow(unused_variables)] + fn read(ptr: *const u32) -> u32 { + unsafe { *ptr } + } "#; // Signature should keep *const u32 let expected = r#" #[doc = "@ lean model read(ptr : Type) ..."] #[allow(unused_variables)] fn read(ptr: *const u32) -> u32 { - if true { ::std::unimplemented!("Safe Shim") } else { ::std::panic!("Contract Violated") } + loop {} } "#; assert_normalized_eq(&transform(input), expected); @@ -454,13 +516,16 @@ mod tests { fn test_generics_preserved() { let input = r#" ///@ lean model ... - unsafe fn cast(x: *const T) -> T { *x } + #[allow(unused_variables)] + fn cast(x: *const T) -> T { + unsafe { *x } + } "#; let expected = r#" #[doc = "@ lean model ..."] #[allow(unused_variables)] fn cast (x: *const T) -> T { - if true { ::std::unimplemented!("Safe Shim") } else { ::std::panic!("Contract Violated") } + loop {} } "#; assert_normalized_eq(&transform(input), expected); @@ -504,18 +569,20 @@ mod tests { #[test] fn test_verification_logic_positive() { - // Wrapper for "Contract Met" let input = r#" ///@ lean model foo ///@ requires x > 0 - unsafe fn foo(x: i32) { } + #[allow(unused_variables)] + fn foo(x: i32) { + unsafe {} + } "#; let expected = r#" #[doc = "@ lean model foo"] #[doc = "@ requires x > 0"] #[allow(unused_variables)] fn foo(x: i32) { - if x > 0 { ::std::unimplemented!("Safe Shim") } else { ::std::panic!("Contract Violated") } + loop {} } "#; assert_normalized_eq(&transform(input), expected); @@ -523,33 +590,43 @@ mod tests { #[test] fn test_verification_logic_negative() { - // Same structure + // Obsolete test for Panic Shim logic. + // We just ensure we generate the loop. let input = r#" ///@ lean model foo ///@ requires x > 0 - unsafe fn foo(x: i32) { } + #[allow(unused_variables)] + fn foo(x: i32) { + unsafe {} + } "#; - let diff = transform(input); - // Normalize for check - let diff_norm: String = diff.chars().filter(|c| !c.is_whitespace()).collect(); - assert!(diff_norm.contains("ifx>0")); - assert!(diff_norm.contains("panic!(\"ContractViolated\")")); + let expected = r#" + #[doc = "@ lean model foo"] + #[doc = "@ requires x > 0"] + #[allow(unused_variables)] + fn foo(x: i32) { + loop {} + } + "#; + assert_normalized_eq(&transform(input), expected); } #[test] fn test_wrong_precondition_trap() { - // Model requires x == 10 let input = r#" ///@ lean model foo ///@ requires x == 10 - unsafe fn foo(x: i32) { } + #[allow(unused_variables)] + fn foo(x: i32) { + unsafe {} + } "#; let expected = r#" #[doc = "@ lean model foo"] #[doc = "@ requires x == 10"] #[allow(unused_variables)] fn foo(x: i32) { - if x == 10 { ::std::unimplemented!("Safe Shim") } else { ::std::panic!("Contract Violated") } + loop {} } "#; assert_normalized_eq(&transform(input), expected); diff --git a/tools/hermes/tests/cases/failure/model_mut_ref.rs b/tools/hermes/tests/cases/failure/model_mut_ref.rs new file mode 100644 index 0000000000..6a62243589 --- /dev/null +++ b/tools/hermes/tests/cases/failure/model_mut_ref.rs @@ -0,0 +1,9 @@ +// @ lean model model_mut_ref(x) +// @ requires true +// @ ensures true +#[allow(unused)] +unsafe fn model_mut_ref(x: &mut u32) { + *x = 0; +} + +fn main() {}