diff --git a/tools/Cargo.lock b/tools/Cargo.lock index 7795e97293..2e1643fb1f 100644 --- a/tools/Cargo.lock +++ b/tools/Cargo.lock @@ -83,7 +83,9 @@ dependencies = [ "anyhow", "cargo_metadata", "clap", + "quote", "regex", + "syn", "walkdir", ] diff --git a/tools/hermes/Cargo.toml b/tools/hermes/Cargo.toml index e97b6e74c7..f6b8d4d46a 100644 --- a/tools/hermes/Cargo.toml +++ b/tools/hermes/Cargo.toml @@ -9,3 +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"] } +quote = "1.0.43" diff --git a/tools/hermes/src/main.rs b/tools/hermes/src/main.rs index c25cdc98cd..a195f6a35c 100644 --- a/tools/hermes/src/main.rs +++ b/tools/hermes/src/main.rs @@ -9,7 +9,7 @@ use std::path::PathBuf; use anyhow::Result; -use cargo_hermes::pipeline::run_pipeline; +use cargo_hermes::pipeline::{Sorry, run_pipeline}; use clap::{Parser, Subcommand}; #[derive(Parser, Debug)] @@ -43,14 +43,19 @@ pub enum Commands { /// Path to Cargo.toml or Cargo script #[arg(long)] manifest_path: Option, + /// Allow missing proofs (substitutes 'sorry') and instruct Lean to accept 'sorry' + #[arg(long)] + allow_sorry: bool, }, } fn main() -> Result<()> { let CargoCli::Hermes(args) = CargoCli::parse(); - let Commands::Verify { crate_name, dest, aeneas_path, manifest_path } = args.command; + let Commands::Verify { crate_name, dest, aeneas_path, manifest_path, allow_sorry } = + args.command; let crate_root = std::env::current_dir()?; let dest = dest.canonicalize()?; - run_pipeline(crate_name, &crate_root, &dest, aeneas_path, manifest_path) + let sorry_mode = if allow_sorry { Sorry::AllowSorry } else { Sorry::RejectSorry }; + run_pipeline(crate_name, &crate_root, &dest, aeneas_path, manifest_path, sorry_mode) } diff --git a/tools/hermes/src/parser.rs b/tools/hermes/src/parser.rs index 8251e672d5..d3e6568d12 100644 --- a/tools/hermes/src/parser.rs +++ b/tools/hermes/src/parser.rs @@ -6,70 +6,188 @@ // This file may not be copied, modified, or distributed except according to // those terms. -use std::sync::LazyLock; +use anyhow::{Result, bail}; +use syn::{ + Attribute, ItemFn, parse_file, + visit::{self, Visit}, +}; -use anyhow::Result; -use regex::Regex; - -/// Represents a specification block extracted from the source code. -/// -/// Contains the function name it applies to and the raw body of the specification. +/// Represents a function parsed from the source code, including its signature and attached specs. #[derive(Debug, Clone)] -pub struct SpecBlock { - pub function_name: String, - pub body: String, +pub struct ParsedFunction { + pub fn_name: String, + pub generics: syn::Generics, + pub spec: Option, + pub proof: Option, } -/// Represents a proof block extracted from the source code. -/// -/// Contains the raw body of the proof. -#[derive(Debug, Clone)] -pub struct ProofBlock { - pub body: String, +pub struct ExtractedBlocks { + pub functions: Vec, } -#[derive(Debug, Clone)] -pub struct ExtractedBlocks { - pub specs: Vec, - pub proofs: Vec, +struct SpecVisitor { + functions: Vec, + errors: Vec, } -/// Extracts both specification and proof blocks from the provided source content. -/// -/// This function uses regular expressions to find blocks formatted as: -/// - `/*@ lean spec function_name ... @*/` -/// - `/*@ proof ... @*/` -pub fn extract_blocks(content: &str) -> Result { - // Regex matches: - // - Start with `/*@` - // - `lean spec` followed by function name - // - Capture function name in `fn_name` - // - Capture content in `body` (non-greedy) - // - End with `@*/` - static SPEC_RE: LazyLock = LazyLock::new(|| { - Regex::new(r"(?ms)/\*\@\s*lean\s+spec\s+(?P\w+)\s+(?P.*?)\s*@\*/").unwrap() - }); - - // Regex matches: - // - Start with `/*@` - // - `proof` - // - Capture content in `body` (non-greedy) - // - End with `@*/` - static PROOF_RE: LazyLock = - LazyLock::new(|| Regex::new(r"(?ms)/\*\@\s*proof\s+(?P.*?)\s*@\*/").unwrap()); - - let mut specs = Vec::new(); - for cap in SPEC_RE.captures_iter(content) { - specs.push(SpecBlock { - function_name: cap["fn_name"].to_string(), - body: cap["body"].trim().to_string(), - }); +impl SpecVisitor { + fn new() -> Self { + Self { functions: Vec::new(), errors: Vec::new() } + } + + fn check_attrs_for_misplaced_spec(&mut self, attrs: &[Attribute], item_kind: &str) { + for attr in attrs { + if let Some(doc_str) = parse_doc_attr(attr) { + if doc_str.trim_start().starts_with("@") { + self.errors.push(anyhow::anyhow!( + "Found `///@` spec usage on a {}, but it is only allowed on functions.", + item_kind + )); + } + } + } } +} + +impl<'ast> Visit<'ast> for SpecVisitor { + fn visit_item_fn(&mut self, node: &'ast ItemFn) { + let fn_name = node.sig.ident.to_string(); + let mut spec_lines = Vec::new(); + let mut proof_lines = Vec::new(); + let mut current_mode = None; // None, Some("spec"), Some("proof") + + for attr in &node.attrs { + if let Some(doc_str) = parse_doc_attr(attr) { + let trimmed = doc_str.trim(); + // Check for ///@ marker (doc comment starting with @) + if trimmed.starts_with('@') { + // Check if it's a new block start + if let Some(content) = trimmed.strip_prefix("@ lean spec") { + 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 + spec_lines.push(content.to_string()); + } else if let Some(content) = trimmed.strip_prefix("@ proof") { + current_mode = Some("proof"); + proof_lines.push(content.to_string()); + } else { + // Continuation line + match current_mode { + Some("spec") => { + // strip leading @ and space? + // User types `///@ ...` -> extracted `@ ...` + // If we just extract `@`, we get ` ...` + // The user might put `///@ ...`. + // If I strip `@`, I get ` ...`. + // I should probably strip the leading `@` and one optional space? + // `trimmed` starts with `@`. + let content = &trimmed[1..]; + spec_lines.push(content.to_string()); + } + Some("proof") => { + let content = &trimmed[1..]; + proof_lines.push(content.to_string()); + } + None => { + // Orphaned @ line? or maybe not meant for us? + self.errors.push(anyhow::anyhow!("Found `///@` line without preceding `lean spec` or `proof` on function '{}'", fn_name)); + } + _ => {} // Should not be possible with current_mode logic + } + } + } + } + } + + 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 let Some(rest) = trimmed_spec.strip_prefix(fn_name.as_str()) { + Some(rest.trim().to_string()) + } else { + Some(trimmed_spec.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 { + fn_name, + generics: node.sig.generics.clone(), + spec, + proof, + }); + } + + // Continue visiting children + visit::visit_item_fn(self, node); + } + + fn visit_item_struct(&mut self, node: &'ast syn::ItemStruct) { + self.check_attrs_for_misplaced_spec(&node.attrs, "struct"); + visit::visit_item_struct(self, node); + } + + fn visit_item_enum(&mut self, node: &'ast syn::ItemEnum) { + self.check_attrs_for_misplaced_spec(&node.attrs, "enum"); + visit::visit_item_enum(self, node); + } + + fn visit_item_mod(&mut self, node: &'ast syn::ItemMod) { + self.check_attrs_for_misplaced_spec(&node.attrs, "module"); + visit::visit_item_mod(self, node); + } + + fn visit_item_const(&mut self, node: &'ast syn::ItemConst) { + self.check_attrs_for_misplaced_spec(&node.attrs, "const"); + visit::visit_item_const(self, node); + } + + // Catch-all for other items with attributes? + // Ideally we'd cover all items, but these are the most common places users might mistakenly put docs. + // Let's also cover TypeAlias and Trait + + fn visit_item_type(&mut self, node: &'ast syn::ItemType) { + self.check_attrs_for_misplaced_spec(&node.attrs, "type alias"); + visit::visit_item_type(self, node); + } + + fn visit_item_trait(&mut self, node: &'ast syn::ItemTrait) { + self.check_attrs_for_misplaced_spec(&node.attrs, "trait"); + visit::visit_item_trait(self, node); + } +} + +fn parse_doc_attr(attr: &Attribute) -> Option { + if !attr.path().is_ident("doc") { + return None; + } + + // syn 2.0: doc = "..." is a NameValue meta + match &attr.meta { + syn::Meta::NameValue(nv) => match &nv.value { + syn::Expr::Lit(syn::ExprLit { lit: syn::Lit::Str(s), .. }) => Some(s.value()), + _ => None, + }, + _ => None, + } +} + +pub fn extract_blocks(content: &str) -> Result { + let ast = parse_file(content)?; + let mut visitor = SpecVisitor::new(); + visitor.visit_file(&ast); - let mut proofs = Vec::new(); - for cap in PROOF_RE.captures_iter(content) { - proofs.push(ProofBlock { body: cap["body"].trim().to_string() }); + if !visitor.errors.is_empty() { + // Return the first error for now, or bundle them + let msg = visitor.errors.iter().map(|e| e.to_string()).collect::>().join("\n"); + bail!("Spec extraction failed:\n{}", msg); } - Ok(ExtractedBlocks { specs, proofs }) + Ok(ExtractedBlocks { functions: visitor.functions }) } diff --git a/tools/hermes/src/pipeline.rs b/tools/hermes/src/pipeline.rs index b077dc0981..47793234ea 100644 --- a/tools/hermes/src/pipeline.rs +++ b/tools/hermes/src/pipeline.rs @@ -16,7 +16,7 @@ use walkdir::WalkDir; use crate::{ orchestration::{run_aeneas, run_charon, run_lake_build}, - parser::{ProofBlock, SpecBlock, extract_blocks}, + parser::{ParsedFunction, extract_blocks}, }; fn get_crate_name( @@ -81,12 +81,19 @@ fn get_crate_name( Err(anyhow!("Could not determine crate name from Cargo.toml")) } +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum Sorry { + AllowSorry, + RejectSorry, +} + pub fn run_pipeline( crate_name: Option, crate_root: &Path, dest: &Path, aeneas_path: Option, manifest_path: Option, + sorry_mode: Sorry, ) -> Result<()> { let crate_name = get_crate_name(manifest_path.as_deref(), crate_name, crate_root)?; @@ -139,13 +146,14 @@ pub fn run_pipeline( &camel_name, dest, manifest_path.as_deref(), + sorry_mode, )?; // 5. Verify println!("Step 4: Verifying..."); // ensure lakefile exists // Note: lakefile still uses snake_case for package name and roots, but `CamelCase` structure for imports - write_lakefile(dest, &crate_name_snake, &camel_name, aeneas_path)?; + write_lakefile(dest, &crate_name_snake, &camel_name, aeneas_path, sorry_mode)?; run_lake_build(dest)?; println!("Verification Successful!"); @@ -158,9 +166,9 @@ fn stitch_user_proofs( crate_name_camel: &str, dest: &Path, source_file: Option<&Path>, + sorry_mode: Sorry, ) -> Result<()> { - let mut all_specs = Vec::new(); - let mut all_proofs = Vec::new(); + let mut all_functions = Vec::new(); if let Some(path) = source_file { // If a specific source file is provided (e.g. script), uses that. @@ -168,8 +176,7 @@ fn stitch_user_proofs( if path.exists() { let content = fs::read_to_string(path)?; let extracted = extract_blocks(&content)?; - all_specs.extend(extracted.specs); - all_proofs.extend(extracted.proofs); + all_functions.extend(extracted.functions); } } else { // Otherwise scan src dir @@ -180,22 +187,21 @@ fn stitch_user_proofs( if entry.path().extension().map_or(false, |ext| ext == "rs") { let content = fs::read_to_string(entry.path())?; let extracted = extract_blocks(&content)?; - all_specs.extend(extracted.specs); - all_proofs.extend(extracted.proofs); + all_functions.extend(extracted.functions); } } } } - generate_lean_file(dest, crate_name_snake, crate_name_camel, &all_specs, &all_proofs) + generate_lean_file(dest, crate_name_snake, crate_name_camel, &all_functions, sorry_mode) } fn generate_lean_file( dest: &Path, namespace_name: &str, import_name: &str, - specs: &[SpecBlock], - proofs: &[ProofBlock], + functions: &[ParsedFunction], + sorry_mode: Sorry, ) -> Result<()> { let mut content = String::new(); content.push_str(&format!("import {}\n", import_name)); @@ -203,52 +209,77 @@ fn generate_lean_file( content.push_str("open Aeneas Aeneas.Std Result Error\n\n"); content.push_str(&format!("open {}\n\n", namespace_name)); - // For the initial version, we assume a strict one-to-one mapping between - // spec blocks and proof blocks. - // Future improvements should support matching by name or more complex interleaving. - // - // The current implementation expects: - // /*@ lean spec ... @*/ - // /*@ proof ... @*/ - // appearing in pairs. - - if specs.len() != proofs.len() { - eprintln!( - "Warning: Number of specs ({}) does not match number of proofs ({})", - specs.len(), - proofs.len() - ); - } + for func in functions { + // Only generate for functions that have a spec. + let spec_body = match &func.spec { + Some(s) => s, + None => continue, + }; - for (i, spec) in specs.iter().enumerate() { - let proof = proofs.get(i).map(|p| p.body.as_str()).unwrap_or("sorry"); + let proof_body = match (&func.proof, sorry_mode) { + (Some(proof), _) => proof.as_str(), + (None, Sorry::AllowSorry) => "sorry", + (None, Sorry::RejectSorry) => anyhow::bail!( + "Missing proof for function '{}'. Use --allow-sorry to fallback to sorry.", + func.fn_name + ), + }; + + // Context Injection + let context = extract_generics_context(&func.generics); // Transform the spec body into a valid Lean theorem type. // If the body contains "ensures", we format it as a return type check. // // Example Input: "ensures |ret| ..." // Example Output: ": ensures |ret| ..." - let body = if spec.body.contains("ensures") && !spec.body.contains(": ensures") { - spec.body.replacen("ensures", ": ensures", 1) + let body = if spec_body.contains("ensures") && !spec_body.contains(": ensures") { + spec_body.replacen("ensures", ": ensures", 1) } else { - spec.body.clone() + spec_body.clone() }; - content.push_str(&format!("theorem {}_spec {}\n", spec.function_name, body)); + content.push_str(&format!("theorem {}_spec {} {}\n", func.fn_name, context, body)); content.push_str(" :=\n"); content.push_str(" by\n"); - content.push_str(proof); + content.push_str(proof_body); content.push_str("\n\n"); } fs::write(dest.join("UserProofs.lean"), content).map_err(Into::into) } +fn extract_generics_context(generics: &syn::Generics) -> String { + let mut context = String::new(); + for param in &generics.params { + if let syn::GenericParam::Type(type_param) = param { + let name = &type_param.ident; + // {T : Type} + context.push_str(&format!("{{{name} : Type}} ")); + + // Bounds + // Simplistic mapping: T: Foo -> [inst : Foo T] + for bound in &type_param.bounds { + if let syn::TypeParamBound::Trait(trait_bound) = bound { + // This is tricky if it's a complex path, but let's try to get the last segment + if let Some(segment) = trait_bound.path.segments.last() { + let trait_name = &segment.ident; + context + .push_str(&format!("[inst{name}{trait_name} : {trait_name} {name}] ")); + } + } + } + } + } + context +} + fn write_lakefile( dest: &Path, crate_name_snake: &str, crate_name_camel: &str, aeneas_path: Option, + sorry_mode: Sorry, ) -> Result<()> { let lakefile_path = dest.join("lakefile.lean"); // Only create if missing. If the user wants to force regen, they should delete it or we add a flag. @@ -258,6 +289,13 @@ fn write_lakefile( r#"require aeneas from git "https://github.com/AeneasVerif/aeneas" @ "main""#.to_string() }; + let more_lean_args = match sorry_mode { + // If sorry is NOT allowed, we want to fail on warnings (like + // 'declaration uses sorry') + Sorry::RejectSorry => "\n moreLeanArgs := #[\"-DwarningAsError=true\"]", + Sorry::AllowSorry => "", + }; + let content = format!( r#" import Lake @@ -269,10 +307,10 @@ package {} @[default_target] lean_lib {} {{ - roots := #[`{}, `UserProofs] + roots := #[`{}, `UserProofs]{} }} "#, - crate_name_snake, require_line, crate_name_snake, crate_name_camel + crate_name_snake, require_line, crate_name_snake, crate_name_camel, more_lean_args ); fs::write(lakefile_path, content).map_err(Into::into) } diff --git a/tools/hermes/tests/cases/failure/checked_add_sorry.rs b/tools/hermes/tests/cases/failure/checked_add_sorry.rs new file mode 100644 index 0000000000..7d2505f37b --- /dev/null +++ b/tools/hermes/tests/cases/failure/checked_add_sorry.rs @@ -0,0 +1,18 @@ +#!/usr/bin/env cargo +//! ```cargo +//! [package] +//! edition = "2021" +//! +//! [dependencies] +//! ``` + +///@ lean spec checked_add (a b : U32) +///@ : ∃ ret, checked_add a b = ok ret ∧ +///@ (match ret with +///@ | none => a.val + b.val > 4294967295 +///@ | some r => r.val = a.val + b.val) +///@ proof sorry +pub fn checked_add(a: u32, b: u32) -> Option { + a.checked_add(b) +} +fn main() {} diff --git a/tools/hermes/tests/cases/failure/incorrect_proof.rs b/tools/hermes/tests/cases/failure/incorrect_proof.rs index e376e8c6c3..574bc944a6 100644 --- a/tools/hermes/tests/cases/failure/incorrect_proof.rs +++ b/tools/hermes/tests/cases/failure/incorrect_proof.rs @@ -8,14 +8,11 @@ //! [dependencies] //! ``` -/*@ lean -spec incorrect (x : U32) -: ∃ ret, incorrect x = ok ret ∧ ret.val = x.val + 1 -@*/ -/*@ proof - simp [incorrect] - -- Error: x != x + 1, so this goal remains unsolved -@*/ +///@ lean spec incorrect (x : U32) +///@ : ∃ ret, incorrect x = ok ret ∧ ret.val = x.val + 1 +///@ proof +///@ simp [incorrect] +///@ -- Error: x != x + 1, so this goal remains unsolved pub fn incorrect(x: u32) -> u32 { x } diff --git a/tools/hermes/tests/cases/failure/missing_proof.rs b/tools/hermes/tests/cases/failure/missing_proof.rs new file mode 100644 index 0000000000..b84b7a3b9d --- /dev/null +++ b/tools/hermes/tests/cases/failure/missing_proof.rs @@ -0,0 +1,7 @@ +///@ lean spec safe_def (x : U32) +///@ : ∃ ret, safe_def x = ok ret +pub fn safe_def(x: u32) -> u32 { + x +} + +fn main() {} diff --git a/tools/hermes/tests/cases/failure/struct_spec.rs b/tools/hermes/tests/cases/failure/struct_spec.rs new file mode 100644 index 0000000000..32edac6c70 --- /dev/null +++ b/tools/hermes/tests/cases/failure/struct_spec.rs @@ -0,0 +1,14 @@ +#!/usr/bin/env cargo +//! ```cargo +//! [package] +//! name = "struct_spec" +//! version = "0.1.0" +//! edition = "2021" +//! +//! [dependencies] +//! ``` + +///@ lean spec foo +struct Foo; + +fn main() {} diff --git a/tools/hermes/tests/cases/failure/syntax_error_in_spec.rs b/tools/hermes/tests/cases/failure/syntax_error_in_spec.rs index c6fbf1605a..474a93ef0a 100644 --- a/tools/hermes/tests/cases/failure/syntax_error_in_spec.rs +++ b/tools/hermes/tests/cases/failure/syntax_error_in_spec.rs @@ -8,10 +8,8 @@ //! [dependencies] //! ``` -/*@ lean -spec syntax_error (x : U32) -: ∃ ret, syntax_error x = ok ret ∧ (((( -@*/ +///@ lean spec syntax_error (x : U32) +///@ : ∃ ret, syntax_error x = ok ret ∧ (((( pub fn syntax_error(x: u32) -> u32 { x } diff --git a/tools/hermes/tests/cases/failure/unchecked_wrapper_sorry.rs b/tools/hermes/tests/cases/failure/unchecked_wrapper_sorry.rs new file mode 100644 index 0000000000..85eaf44b1f --- /dev/null +++ b/tools/hermes/tests/cases/failure/unchecked_wrapper_sorry.rs @@ -0,0 +1,38 @@ +#!/usr/bin/env cargo +//! ```cargo +//! [package] +//! name = "unchecked_wrapper" +//! version = "0.1.0" +//! edition = "2021" +//! +//! [dependencies] +//! ``` + +///@ lean spec raw_inc (x : U32) +///@ : ∃ ret, raw_inc x = ok ret ∧ ret.val = x.val + 1 +///@ proof sorry +#[allow(unused_unsafe)] +unsafe fn raw_inc(x: u32) -> u32 { + unsafe { x + 1 } +} + +///@ lean spec safe_inc (x : U32) +///@ : ∃ ret, safe_inc x = ok ret ∧ +///@ (if x.val < U32.rMax then ret.val = x.val + 1 else ret.val = 0) +///@ proof +///@ simp [safe_inc] +///@ split +///@ case isTrue h => +///@ have ⟨ret, h_call, h_val⟩ := raw_inc_spec x +///@ rw [h_call] +///@ simp_all +///@ case isFalse h => +///@ simp +pub fn safe_inc(x: u32) -> u32 { + if x < u32::MAX { + unsafe { raw_inc(x) } + } else { + 0 + } +} +fn main() {} diff --git a/tools/hermes/tests/cases/failure/undefined_variable.rs b/tools/hermes/tests/cases/failure/undefined_variable.rs index 9fc68802ad..bf50906cba 100644 --- a/tools/hermes/tests/cases/failure/undefined_variable.rs +++ b/tools/hermes/tests/cases/failure/undefined_variable.rs @@ -8,10 +8,8 @@ //! [dependencies] //! ``` -/*@ lean -spec undefined_var (x : u32) -ensures |ret| ret.val = y.val -- y is undefined -@*/ +///@ lean spec undefined_var (x : u32) +///@ ensures |ret| ret.val = y.val -- y is undefined pub fn undefined_var(x: u32) -> u32 { x } diff --git a/tools/hermes/tests/cases/success/add.rs b/tools/hermes/tests/cases/success/add.rs index 6b13bb6e09..62157e7aa7 100644 --- a/tools/hermes/tests/cases/success/add.rs +++ b/tools/hermes/tests/cases/success/add.rs @@ -8,13 +8,10 @@ //! [dependencies] //! ``` -/*@ lean -spec add (a b : U32) -: ∃ ret, add a b = ok ret ∧ ret.val = (a.val + b.val) % 4294967296 -@*/ -/*@ proof - sorry -@*/ +///@ lean spec add (a b : U32) +///@ : ∃ ret, add a b = ok ret ∧ ret.val = (a.val + b.val) % U32.size +///@ proof +///@ simp [add] pub fn add(a: u32, b: u32) -> u32 { a.wrapping_add(b) } diff --git a/tools/hermes/tests/cases/success/checked_add.rs b/tools/hermes/tests/cases/success/checked_add.rs deleted file mode 100644 index 775f4fd337..0000000000 --- a/tools/hermes/tests/cases/success/checked_add.rs +++ /dev/null @@ -1,22 +0,0 @@ -#!/usr/bin/env cargo -//! ```cargo -//! [package] -//! edition = "2021" -//! -//! [dependencies] -//! ``` - -/*@ lean -spec checked_add (a b : U32) -: ∃ ret, checked_add a b = ok ret ∧ - (match ret with - | none => a.val + b.val > 4294967295 - | some r => r.val = a.val + b.val) -@*/ -/*@ proof - sorry -@*/ -pub fn checked_add(a: u32, b: u32) -> Option { - a.checked_add(b) -} -fn main() {} diff --git a/tools/hermes/tests/cases/success/generic_id.rs b/tools/hermes/tests/cases/success/generic_id.rs index 0cb18b4e9b..ca16559362 100644 --- a/tools/hermes/tests/cases/success/generic_id.rs +++ b/tools/hermes/tests/cases/success/generic_id.rs @@ -8,21 +8,10 @@ //! [dependencies] //! ``` -/*@ lean -<<<<<<< Updated upstream -spec id (T : Type) (x : T) -: id T x = ok x -@*/ -/*@ proof -======= -spec id {T : Type} (x : T) -ensures |ret| ret = x -@*/ -/*@ proof -:= by ->>>>>>> Stashed changes - simp [id] -@*/ +///@ lean spec id (x : T) +///@ : generic_id.id x = ok x +///@ proof +///@ simp [generic_id.id] pub fn id(x: T) -> T { x } diff --git a/tools/hermes/tests/cases/success/struct_method.rs b/tools/hermes/tests/cases/success/struct_method.rs index 93dadae3d4..e082c88b94 100644 --- a/tools/hermes/tests/cases/success/struct_method.rs +++ b/tools/hermes/tests/cases/success/struct_method.rs @@ -13,28 +13,13 @@ pub struct Point { pub y: u32, } -/*@ lean -<<<<<<< Updated upstream -spec move_pt (self : Point) (dx dy : U32) -: ∃ self_final, move_pt self dx dy = ok ((), self_final) ∧ - self_final.x.val = self.x.val + dx.val ∧ - self_final.y.val = self.y.val + dy.val -@*/ -/*@ proof - sorry -======= -spec move_pt (self : Point) (dx dy : u32) -ensures |ret, self_final| - ret = () /\ self_final.x.val = self.x.val + dx.val /\ self_final.y.val = self.y.val + dy.val -@*/ -/*@ proof -:= by - simp [move_pt] - simp [nop_div_pt] -- Aeneas might generate different names? - linarith ->>>>>>> Stashed changes -@*/ impl Point { + ///@ lean spec move_pt (self : Point) (dx dy : u32) + ///@ ensures |ret, self_final| + ///@ ret = () /\ self_final.x.val = self.x.val + dx.val /\ self_final.y.val = self.y.val + dy.val + ///@ proof + ///@ simp [move_pt] + ///@ linarith pub fn move_pt(&mut self, dx: u32, dy: u32) { self.x += dx; self.y += dy; diff --git a/tools/hermes/tests/cases/success/unchecked_wrapper.rs b/tools/hermes/tests/cases/success/unchecked_wrapper.rs deleted file mode 100644 index 96daf460b9..0000000000 --- a/tools/hermes/tests/cases/success/unchecked_wrapper.rs +++ /dev/null @@ -1,57 +0,0 @@ -#!/usr/bin/env cargo -//! ```cargo -//! [package] -//! name = "unchecked_wrapper" -//! version = "0.1.0" -//! edition = "2021" -//! -//! [dependencies] -//! ``` - -/*@ lean -<<<<<<< Updated upstream -spec raw_inc (x : U32) -: ∃ ret, raw_inc x = ok ret ∧ ret.val = x.val + 1 -======= -model raw_inc (x : u32) -requires h_safe : x.val < 4294967295 -ensures |ret| ret.val = x.val + 1 ->>>>>>> Stashed changes -@*/ -#[allow(unused_unsafe)] -unsafe fn raw_inc(x: u32) -> u32 { - unsafe { x + 1 } -} - -/*@ lean -<<<<<<< Updated upstream -spec safe_inc (x : U32) -: ∃ ret, safe_inc x = ok ret ∧ - (if x.val < 4294967295 then ret.val = x.val + 1 else ret.val = 0) -@*/ -/*@ proof - sorry -======= -spec safe_inc (x : u32) - ensures |ret| - if x.val < 4294967295 then ret.val = x.val + 1 else ret.val = 0 -@*/ -/*@ proof -:= by - simp [safe_inc] - split - case inl h => - simp [raw_inc] - simp [h] - case inr h => - simp ->>>>>>> Stashed changes -@*/ -pub fn safe_inc(x: u32) -> u32 { - if x < u32::MAX { - unsafe { raw_inc(x) } - } else { - 0 - } -} -fn main() {} diff --git a/tools/hermes/tests/integration.rs b/tools/hermes/tests/integration.rs index d08961916c..b717830835 100644 --- a/tools/hermes/tests/integration.rs +++ b/tools/hermes/tests/integration.rs @@ -12,7 +12,7 @@ use std::{ path::{Path, PathBuf}, }; -use cargo_hermes::pipeline::run_pipeline; +use cargo_hermes::pipeline::{Sorry, run_pipeline}; struct TestTempDir { path: PathBuf, @@ -90,8 +90,19 @@ fn run_suite(suite_name: &str, expect_success: bool) { let path = entry.path(); if path.extension().map_or(false, |e| e == "rs") { let file_name = path.file_stem().unwrap().to_string_lossy().to_string(); + if let Ok(filter) = env::var("HERMES_FILTER") { + if !file_name.contains(&filter) { + continue; + } + } println!("Running {} test case: {:?}", suite_name, path.file_name().unwrap()); - run_case(&path, &aeneas_lean_path, Some(file_name), expect_success); + run_case( + &path, + &aeneas_lean_path, + Some(file_name), + expect_success, + Sorry::RejectSorry, + ); } } } @@ -101,6 +112,12 @@ fn run_suite(suite_name: &str, expect_success: bool) { fn test_integration_suite() { run_suite("success", true); run_suite("failure", false); + + // Should succeed with allow_sorry=true + let (cases_dir, aeneas_lean_path) = setup_env(); + let path = cases_dir.join("failure/missing_proof.rs"); + println!("Running allow_sorry test case: {:?}", path.file_name().unwrap()); + run_case(&path, &aeneas_lean_path, Some("missing_proof".to_string()), true, Sorry::AllowSorry); } fn run_case( @@ -108,18 +125,59 @@ fn run_case( aeneas_path: &Path, crate_name: Option, expect_success: bool, + sorry_mode: Sorry, ) { let temp_dir = TestTempDir::new(); let crate_root = temp_dir.path(); + let shared_packages = crate_root.join("shared_lake_packages"); + fs::create_dir_all(&shared_packages).expect("Failed to create shared packages dir"); + let shared_build = crate_root.join("shared_lake_build"); + fs::create_dir_all(&shared_build).expect("Failed to create shared build dir"); + // Run pipeline directly on the script source path - let dest = crate_root.join("verification"); + let dest = crate_root + .join("verification") + .join(crate_name.clone().unwrap_or_else(|| "unknown".to_string())); + + // Pre-create .lake structure + let dest_lake = dest.join(".lake"); + fs::create_dir_all(&dest_lake).expect("Failed to create .lake dir"); + + let dest_packages = dest_lake.join("packages"); + // Force symlink packages + if dest_packages.exists() { + if !dest_packages.is_symlink() { + fs::remove_dir_all(&dest_packages).expect("Failed to remove existing packages dir"); + } + } + if !dest_packages.exists() { + std::os::unix::fs::symlink(&shared_packages, &dest_packages) + .expect("Failed to symlink packages"); + } + + let dest_build = dest_lake.join("build"); + // Force symlink build + if dest_build.exists() { + if !dest_build.is_symlink() { + if dest_build.is_dir() { + fs::remove_dir_all(&dest_build).expect("Failed to remove existing build dir"); + } else { + fs::remove_file(&dest_build).expect("Failed to remove existing build file"); + } + } + } + if !dest_build.exists() { + std::os::unix::fs::symlink(&shared_build, &dest_build).expect("Failed to symlink build"); + } + let result = run_pipeline( crate_name.clone(), crate_root, &dest, Some(aeneas_path.to_path_buf()), Some(source_path.to_path_buf()), + sorry_mode, ); if expect_success {