From 9a2da1262f079e7bbeea00d7754ee591b66d306e Mon Sep 17 00:00:00 2001 From: Joshua Liebow-Feeser Date: Tue, 3 Feb 2026 01:06:37 +0000 Subject: [PATCH] [WIP] Shadow crate + unsafe gherrit-pr-id: Gb85ad5e55a47c49ab2c049a2ec5972fc6d082e31 --- tools/hermes/Cargo.toml | 2 +- tools/hermes/src/lib.rs | 1 + tools/hermes/src/parser.rs | 21 +- tools/hermes/src/pipeline.rs | 79 ++- tools/hermes/src/shadow.rs | 528 ++++++++++++++++++ .../tests/cases/failure/checked_add_sorry.rs | 3 +- .../tests/cases/failure/incorrect_proof.rs | 2 +- .../cases/failure/shadow_contract_fail.rs | 25 + .../tests/cases/failure/shadow_prec_fail.rs | 21 + .../hermes/tests/cases/failure/struct_spec.rs | 2 +- .../cases/failure/syntax_error_in_spec.rs | 2 +- .../cases/failure/unchecked_wrapper_sorry.rs | 9 +- .../tests/cases/failure/undefined_variable.rs | 2 +- .../hermes/tests/cases/success/generic_id.rs | 3 +- .../tests/cases/success/shadow_model.rs | 21 + .../tests/cases/success/struct_method.rs | 3 +- 16 files changed, 667 insertions(+), 57 deletions(-) create mode 100644 tools/hermes/src/shadow.rs create mode 100644 tools/hermes/tests/cases/failure/shadow_contract_fail.rs create mode 100644 tools/hermes/tests/cases/failure/shadow_prec_fail.rs create mode 100644 tools/hermes/tests/cases/success/shadow_model.rs diff --git a/tools/hermes/Cargo.toml b/tools/hermes/Cargo.toml index f6b8d4d46a..672936a5b3 100644 --- a/tools/hermes/Cargo.toml +++ b/tools/hermes/Cargo.toml @@ -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" diff --git a/tools/hermes/src/lib.rs b/tools/hermes/src/lib.rs index 960a232e56..f9727fbf70 100644 --- a/tools/hermes/src/lib.rs +++ b/tools/hermes/src/lib.rs @@ -17,4 +17,5 @@ pub mod desugar; pub mod orchestration; pub mod parser; pub mod pipeline; +pub mod shadow; pub mod translator; diff --git a/tools/hermes/src/parser.rs b/tools/hermes/src/parser.rs index e4c253ec4d..cc9b006da9 100644 --- a/tools/hermes/src/parser.rs +++ b/tools/hermes/src/parser.rs @@ -18,6 +18,7 @@ pub struct ParsedFunction { pub sig: syn::Signature, pub spec: Option, pub proof: Option, + pub is_model: bool, } pub struct ExtractedBlocks { @@ -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) { @@ -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"); @@ -95,15 +94,7 @@ 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 }; @@ -111,7 +102,7 @@ impl<'ast> Visit<'ast> for SpecVisitor { 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) diff --git a/tools/hermes/src/pipeline.rs b/tools/hermes/src/pipeline.rs index f0f7584e4b..82fdd199e1 100644 --- a/tools/hermes/src/pipeline.rs +++ b/tools/hermes/src/pipeline.rs @@ -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()) + } + } 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)); @@ -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)?; @@ -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, @@ -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 ), @@ -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"); } diff --git a/tools/hermes/src/shadow.rs b/tools/hermes/src/shadow.rs new file mode 100644 index 0000000000..91a2482f01 --- /dev/null +++ b/tools/hermes/src/shadow.rs @@ -0,0 +1,528 @@ +// Copyright 2026 The Fuchsia Authors +// +// Licensed under a BSD-style license , Apache License, Version 2.0 +// , or the MIT +// license , at your option. +// This file may not be copied, modified, or distributed except according to +// those terms. + +use std::{ + fs, + path::{Path, PathBuf}, +}; + +use anyhow::{Context, Result}; +use quote::quote; +use syn::{Attribute, Expr, ExprBlock, ItemFn, parse_quote, visit_mut::VisitMut}; +use walkdir::WalkDir; + +pub fn create_shadow_crate( + original_root: &Path, + source_file: Option<&Path>, +) -> Result<(PathBuf, Option)> { + // 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::create_dir_all(&shadow_root).context("Failed to create shadow directory")?; + + // 2. Recursive Copy (only if not a single-file script, OR generally?) + // If it's a script, original_root might be unrelated. + // However, if we preserve behaviour, we might want to copy cargo lock etc? + + // Copy Cargo.toml + let cargo_toml = original_root.join("Cargo.toml"); + if cargo_toml.exists() { + fs::copy(&cargo_toml, shadow_root.join("Cargo.toml")) + .context("Failed to copy Cargo.toml")?; + } + + // Copy Cargo.lock if exists + let cargo_lock = original_root.join("Cargo.lock"); + if cargo_lock.exists() { + fs::copy(&cargo_lock, shadow_root.join("Cargo.lock")).ok(); + } + + // Copy src/ recursively + let src_path = original_root.join("src"); + if src_path.exists() { + let dest_src = shadow_root.join("src"); + fs::create_dir_all(&dest_src)?; + + for entry in WalkDir::new(&src_path) { + let entry = entry?; + let relative = entry.path().strip_prefix(&src_path)?; + let dest_path = dest_src.join(relative); + + if entry.file_type().is_dir() { + fs::create_dir_all(&dest_path)?; + } else if entry.file_type().is_file() { + fs::copy(entry.path(), &dest_path)?; + } + } + } + + // 3. Sanitization + sanitize_crate(&shadow_root)?; + + // 4. Handle Single Source File + let shadow_source_file = if let Some(source) = source_file { + let file_name = source.file_name().context("Invalid source file name")?; + let dest_path = shadow_root.join(file_name); + + // Sanitize and write + process_file_content(source, &dest_path)?; + Some(dest_path) + } else { + None + }; + + Ok((shadow_root, shadow_source_file)) +} + +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; + visitor.visit_file_mut(&mut ast); + + let new_content = quote!(#ast).to_string(); + fs::write(dest, new_content)?; + Ok(()) +} + +fn sanitize_crate(root: &Path) -> Result<()> { + let src_dir = root.join("src"); + if !src_dir.exists() { + return Ok(()); + } + + for entry in WalkDir::new(&src_dir) { + let entry = entry?; + if entry.file_type().is_file() && entry.path().extension().map_or(false, |e| e == "rs") { + process_file(entry.path())?; + } + } + Ok(()) +} + +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; + visitor.visit_file_mut(&mut ast); + + let new_content = quote!(#ast).to_string(); + fs::write(path, new_content)?; + Ok(()) +} + +struct ShadowVisitor; + +impl VisitMut for ShadowVisitor { + fn visit_item_fn_mut(&mut self, node: &mut ItemFn) { + let (is_model, model_requires) = parse_model_specs(&node.attrs); + + // We only care about `unsafe fn` + 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 { + unimplemented!("Safe Shim") + } else { + panic!("Contract Violated") + } + } + }; + + // Replace body + if let Ok(block) = syn::parse2(body_content) { + node.block = block; + } + } 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); + } + } else { + // Safe function: just recurse + syn::visit_mut::visit_item_fn_mut(self, node); + } + } + + fn visit_expr_mut(&mut self, node: &mut Expr) { + if let Expr::Unsafe(expr_unsafe) = node { + // Transform `unsafe { ... }` into `{ ... }` + // We preserve attributes and the inner block + let new_expr = Expr::Block(ExprBlock { + attrs: expr_unsafe.attrs.clone(), + label: None, + block: expr_unsafe.block.clone(), + }); + *node = new_expr; + + // Recurse into the new block (in case there are nested unsafe blocks) + self.visit_expr_mut(node); + } else { + syn::visit_mut::visit_expr_mut(self, node); + } + } +} + +fn parse_doc_attr(attr: &Attribute) -> Option { + if !attr.path().is_ident("doc") { + return None; + } + 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, + } +} + +fn parse_model_specs(attrs: &[Attribute]) -> (bool, Vec) { + let mut is_model = false; + let mut requires = Vec::new(); + + for attr in attrs { + if let Some(doc) = parse_doc_attr(attr) { + println!("DEBUG: Doc attr: {:?}", doc); + for line in doc.lines() { + let trimmed = line.trim(); + println!("DEBUG: Trimmed line: '{}'", trimmed); + // Check found marker e.g. "@ lean model" + if trimmed.starts_with('@') { + if trimmed.contains("lean model") { + is_model = true; + println!("DEBUG: Found model marker!"); + } + + if let Some(rest) = trimmed.strip_prefix("@ requires") { + let content = rest.trim(); + // Strip binder name if present (e.g. "h : x > 0" -> "x > 0") + let condition = if let Some((_, expr)) = content.split_once(':') { + expr.trim() + } else { + content + }; + requires.push(condition.to_string()); + } + } + } + } + } + (is_model, requires) +} + +#[cfg(test)] +mod tests { + use quote::quote; + + use super::*; + + fn transform(code: &str) -> String { + let mut ast = syn::parse_file(code).expect("Failed to parse input"); + let mut visitor = ShadowVisitor; + visitor.visit_file_mut(&mut ast); + quote!(#ast).to_string() + } + + fn assert_normalized_eq(actual: &str, expected: &str) { + let actual_norm: String = actual.chars().filter(|c| !c.is_whitespace()).collect(); + let expected_norm: String = expected.chars().filter(|c| !c.is_whitespace()).collect(); + assert_eq!( + actual_norm, expected_norm, + "\nExpected(norm): {}\nActual(norm): {}\n\nOriginal Actual:\n{}", + expected_norm, actual_norm, actual + ); + } + + // Category 1: Leaf Node (Model Strategy) + + #[test] + fn test_leaf_node_basic() { + let input = r#" + ///@ lean model foo ensures |ret| ret = 42 + unsafe fn foo() -> i32 { unsafe { *ptr } } + "#; + let expected = r#" + #[doc = "@ lean model foo ensures |ret| ret = 42"] + fn foo() -> i32 { + if true { unimplemented!("Safe Shim") } else { panic!("Contract Violated") } + } + "#; + assert_normalized_eq(&transform(input), expected); + } + + #[test] + fn test_leaf_node_preconditions() { + let input = r#" + ///@ lean model safe_div(a b : u32) + ///@ requires b > 0 + unsafe fn safe_div(a: u32, b: u32) -> u32 { 0 } + "#; + let expected = r#" + #[doc = "@ lean model safe_div(a b : u32)"] + #[doc = "@ requires b > 0"] + fn safe_div(a: u32, b: u32) -> u32 { + if (b > 0) { unimplemented!("Safe Shim") } else { panic!("Contract Violated") } + } + "#; + assert_normalized_eq(&transform(input), expected); + } + + #[test] + fn test_raw_pointer_signatures() { + let input = r#" + ///@ lean model read(ptr : Type) ... + unsafe fn read(ptr: *const u32) -> u32 { *ptr } + "#; + // Signature should keep *const u32 + let expected = r#" + #[doc = "@ lean model read(ptr : Type) ..."] + fn read(ptr: *const u32) -> u32 { + if true { unimplemented!("Safe Shim") } else { panic!("Contract Violated") } + } + "#; + assert_normalized_eq(&transform(input), expected); + } + + // Category 2: Intermediate Node (Unwrap Strategy) + + #[test] + fn test_structural_unwrap() { + let input = r#" + unsafe fn wrapper() { + unsafe { foo() } + } + "#; + // Note: visitor transforms `unsafe { block }` -> `{ block }` + let expected = r#" + fn wrapper() { + { foo() } + } + "#; + assert_normalized_eq(&transform(input), expected); + } + + #[test] + fn test_block_scoping() { + let input = r#" + fn main() { + let x = 1; + unsafe { + let x = 2; + use_val(x); + } + use_val(x); + } + "#; + let expected = r#" + fn main() { + let x = 1; + { + let x = 2; + use_val(x); + } + use_val(x); + } + "#; + assert_normalized_eq(&transform(input), expected); + } + + #[test] + fn test_expr_unsafe_block() { + let input = r#" + fn main() { + let y = unsafe { + let z = 10; + z * 2 + }; + } + "#; + let expected = r#" + fn main() { + let y = { + let z = 10; + z * 2 + }; + } + "#; + assert_normalized_eq(&transform(input), expected); + } + + // Category 3: Complex Rust Features + + #[test] + fn test_generics_preserved() { + let input = r#" + ///@ lean model ... + unsafe fn cast(x: *const T) -> T { *x } + "#; + let expected = r#" + #[doc = "@ lean model ..."] + fn cast (x: *const T) -> T { + if true { unimplemented!("Safe Shim") } else { panic!("Contract Violated") } + } + "#; + assert_normalized_eq(&transform(input), expected); + } + + #[test] + fn test_unsafe_trait_impl() { + let input = r#" + unsafe impl GlobalAlloc for MyAllocator { } + "#; + // Visitor is structural on Fn and Expr, usually ignores ItemImpl unless recurse + // We only implemented visit_item_fn_mut and visit_expr_mut + // Default visit_item_impl_mut recurses. + // It shouldn't change `unsafe impl`. + let expected = input; + assert_normalized_eq(&transform(input), expected); + } + + #[test] + fn test_nested_unsafe() { + let input = r#" + fn nesting() { + unsafe { + let ptr = 0 as *const i32; + unsafe { *ptr } + } + } + "#; + let expected = r#" + fn nesting() { + { + let ptr = 0 as *const i32; + { *ptr } + } + } + "#; + assert_normalized_eq(&transform(input), expected); + } + + // Category 4: Verification Logic (Proof 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) { } + "#; + let expected = r#" + #[doc = "@ lean model foo"] + #[doc = "@ requires x > 0"] + fn foo(x: i32) { + if (x > 0) { unimplemented!("Safe Shim") } else { panic!("Contract Violated") } + } + "#; + assert_normalized_eq(&transform(input), expected); + } + + #[test] + fn test_verification_logic_negative() { + // Same structure + let input = r#" + ///@ lean model foo + ///@ requires x > 0 + unsafe fn foo(x: i32) { } + "#; + let diff = transform(input); + // Normalize for check + let diff_norm: String = diff.chars().filter(|c| !c.is_whitespace()).collect(); + assert!(diff_norm.contains("if(x>0)")); + assert!(diff_norm.contains("panic!(\"ContractViolated\")")); + } + + #[test] + fn test_wrong_precondition_trap() { + // Model requires x == 10 + let input = r#" + ///@ lean model foo + ///@ requires x == 10 + unsafe fn foo(x: i32) { } + "#; + let expected = r#" + #[doc = "@ lean model foo"] + #[doc = "@ requires x == 10"] + fn foo(x: i32) { + if (x == 10) { unimplemented!("Safe Shim") } else { panic!("Contract Violated") } + } + "#; + assert_normalized_eq(&transform(input), expected); + } + + // Category 5: Syntactic Edge Cases + + #[test] + fn test_attributes_preserved() { + let input = r#" + fn main() { + #[allow(unused_unsafe)] + unsafe { } + } + "#; + let expected = r#" + fn main() { + #[allow(unused_unsafe)] + { } + } + "#; + assert_normalized_eq(&transform(input), expected); + } + + #[test] + fn test_doc_comments_preserved() { + let input = r#" + /// Doc comment + unsafe fn foo() { } + "#; + // Unwrap strategy - quote expands doc comments to attributes + let expected = r#" + #[doc = " Doc comment"] + fn foo() { } + "#; + assert_normalized_eq(&transform(input), expected); + } + + #[test] + fn test_macro_invoking_unsafe() { + let input = r#" + fn main() { + my_unsafe_macro!(); + } + "#; + // Should be untouched + assert_normalized_eq(&transform(input), input); + } +} diff --git a/tools/hermes/tests/cases/failure/checked_add_sorry.rs b/tools/hermes/tests/cases/failure/checked_add_sorry.rs index ccacf7d004..88dc0af795 100644 --- a/tools/hermes/tests/cases/failure/checked_add_sorry.rs +++ b/tools/hermes/tests/cases/failure/checked_add_sorry.rs @@ -2,7 +2,7 @@ //! ```cargo //! [package] //! edition = "2021" -//! +//! //! [dependencies] //! ``` @@ -14,4 +14,5 @@ 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 7664cd76f6..7666abd21c 100644 --- a/tools/hermes/tests/cases/failure/incorrect_proof.rs +++ b/tools/hermes/tests/cases/failure/incorrect_proof.rs @@ -4,7 +4,7 @@ //! name = "incorrect_proof" //! version = "0.1.0" //! edition = "2021" -//! +//! //! [dependencies] //! ``` diff --git a/tools/hermes/tests/cases/failure/shadow_contract_fail.rs b/tools/hermes/tests/cases/failure/shadow_contract_fail.rs new file mode 100644 index 0000000000..c0e0c7c121 --- /dev/null +++ b/tools/hermes/tests/cases/failure/shadow_contract_fail.rs @@ -0,0 +1,25 @@ +///@ lean model check_pos(x : U32) +///@ requires h : x > 0 +///@ ensures |ret| ret = x +pub unsafe fn check_pos(x: u32) -> u32 { + unsafe { + if x == 0 { + std::hint::unreachable_unchecked() + } + x + } +} + +///@ lean spec wrapper_fail (x : U32) +///@ ensures |ret| ret.val = 0 +///@ proof +///@ intros +///@ simp [wrapper_fail] +pub fn wrapper_fail(x: u32) -> u32 { + // VIOLATION: Calling check_pos(0) when it requires x > 0 + // This should fail to prove because the shim panics (Result.fail) + // while the spec expects a return value. + unsafe { check_pos(0) } +} + +fn main() {} diff --git a/tools/hermes/tests/cases/failure/shadow_prec_fail.rs b/tools/hermes/tests/cases/failure/shadow_prec_fail.rs new file mode 100644 index 0000000000..5278971cc3 --- /dev/null +++ b/tools/hermes/tests/cases/failure/shadow_prec_fail.rs @@ -0,0 +1,21 @@ +///@ lean model must_be_ten(x : U32) +///@ requires h : x == 10 +///@ ensures |ret| ret.val = 10 +pub unsafe fn must_be_ten(x: u32) -> u32 { + x +} + +///@ lean spec prec_trap (x : U32) +///@ requires x.val > 10 +///@ ensures |ret| ret.val = 10 +///@ proof +///@ intros +///@ simp [prec_trap] +pub fn prec_trap(x: u32) -> u32 { + // TRAP: x > 10 does not imply x = 10 + // We satisfy *a* condition (x > 10), but not the *required* one (x = 10) + // Verification should fail. + unsafe { must_be_ten(x) } +} + +fn main() {} diff --git a/tools/hermes/tests/cases/failure/struct_spec.rs b/tools/hermes/tests/cases/failure/struct_spec.rs index 32edac6c70..d51f90c1d6 100644 --- a/tools/hermes/tests/cases/failure/struct_spec.rs +++ b/tools/hermes/tests/cases/failure/struct_spec.rs @@ -4,7 +4,7 @@ //! name = "struct_spec" //! version = "0.1.0" //! edition = "2021" -//! +//! //! [dependencies] //! ``` 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 4a18cb3b7e..103d879e41 100644 --- a/tools/hermes/tests/cases/failure/syntax_error_in_spec.rs +++ b/tools/hermes/tests/cases/failure/syntax_error_in_spec.rs @@ -4,7 +4,7 @@ //! name = "syntax_error_in_spec" //! version = "0.1.0" //! edition = "2021" -//! +//! //! [dependencies] //! ``` diff --git a/tools/hermes/tests/cases/failure/unchecked_wrapper_sorry.rs b/tools/hermes/tests/cases/failure/unchecked_wrapper_sorry.rs index 3eaeb3cbaa..2418215e7a 100644 --- a/tools/hermes/tests/cases/failure/unchecked_wrapper_sorry.rs +++ b/tools/hermes/tests/cases/failure/unchecked_wrapper_sorry.rs @@ -4,7 +4,7 @@ //! name = "unchecked_wrapper" //! version = "0.1.0" //! edition = "2021" -//! +//! //! [dependencies] //! ``` @@ -28,10 +28,7 @@ unsafe fn raw_inc(x: u32) -> u32 { ///@ case isFalse h => ///@ simp pub fn safe_inc(x: u32) -> u32 { - if x < u32::MAX { - unsafe { raw_inc(x) } - } else { - 0 - } + 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 bf50906cba..2b60848e86 100644 --- a/tools/hermes/tests/cases/failure/undefined_variable.rs +++ b/tools/hermes/tests/cases/failure/undefined_variable.rs @@ -4,7 +4,7 @@ //! name = "undefined_variable" //! version = "0.1.0" //! edition = "2021" -//! +//! //! [dependencies] //! ``` diff --git a/tools/hermes/tests/cases/success/generic_id.rs b/tools/hermes/tests/cases/success/generic_id.rs index 08ff2e00f7..1cdf006435 100644 --- a/tools/hermes/tests/cases/success/generic_id.rs +++ b/tools/hermes/tests/cases/success/generic_id.rs @@ -4,7 +4,7 @@ //! name = "generic_id" //! version = "0.1.0" //! edition = "2021" -//! +//! //! [dependencies] //! ``` @@ -15,4 +15,5 @@ pub fn id(x: T) -> T { x } + fn main() {} diff --git a/tools/hermes/tests/cases/success/shadow_model.rs b/tools/hermes/tests/cases/success/shadow_model.rs new file mode 100644 index 0000000000..7f8942dc16 --- /dev/null +++ b/tools/hermes/tests/cases/success/shadow_model.rs @@ -0,0 +1,21 @@ +///@ lean model safe_div(a b : U32) +///@ requires h : b > 0 +///@ ensures |ret| ret.val = a.val / b.val +pub unsafe fn safe_div(a: u32, b: u32) -> u32 { + unsafe { a / b } +} + +///@ lean spec wrapper (a : U32) +///@ ensures |ret| ret.val = a.val +///@ proof +///@ rw [wrapper] +///@ have ⟨ ret, h ⟩ := safe_div_spec a 1#u32 (by native_decide) +///@ simp [h.1] +///@ simp_all [Nat.div_one, h.2] +pub fn wrapper(a: u32) -> u32 { + // Calling safe_div with valid input + // The unsafe block should be removed/shimmed in shadow crate + unsafe { safe_div(a, 1) } +} + +fn main() {} diff --git a/tools/hermes/tests/cases/success/struct_method.rs b/tools/hermes/tests/cases/success/struct_method.rs index e082c88b94..9debb61334 100644 --- a/tools/hermes/tests/cases/success/struct_method.rs +++ b/tools/hermes/tests/cases/success/struct_method.rs @@ -4,7 +4,7 @@ //! name = "struct_method" //! version = "0.1.0" //! edition = "2021" -//! +//! //! [dependencies] //! ``` @@ -25,4 +25,5 @@ impl Point { self.y += dy; } } + fn main() {}