[WIP] Model unsafe functions as noncomputable

tools/hermes/src/desugar.rs

@@ -6,6 +6,8 @@ pub struct DesugaredSpec {
     pub signature_args: Option<String>,
     pub extra_args: Vec<String>, // e.g., (h_safe : ...)
     pub body: String,
+    pub predicate: Option<String>,
+    pub binders: Vec<String>,
 }
 
 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>, String)> {
+pub fn parse_binders(ensures_content: &str) -> Result<(Vec<String>, String)> {
     // |ret, x_final| logic
     if let Some(start) = ensures_content.find('|')
         && let Some(end) = ensures_content[start + 1..].find('|')

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<T>(src: *const T) -> T {
-        unsafe { ::std::ptr::read(src) }
+        loop {}
     }
 }
 

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.")?;