cache results of formal proofs

Cargo.lock

@@ -69,6 +69,18 @@ dependencies = [
  "windows-sys 0.52.0",
 ]
 
+[[package]]
+name = "arrayref"
+version = "0.3.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "76a2e8124351fda1ef8aaaa3bbd7ebbcb486bbcd4225aca0aa0d84bb2db8fecb"
+
+[[package]]
+name = "arrayvec"
+version = "0.7.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7c02d123df017efcdfbd739ef81735b36c5ba83ec3c59c80a9d7ecc718f92e50"
+
 [[package]]
 name = "autocfg"
 version = "1.1.0"
@@ -109,6 +121,20 @@ dependencies = [
  "wyz",
 ]
 
+[[package]]
+name = "blake3"
+version = "1.5.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d82033247fd8e890df8f740e407ad4d038debb9eb1f40533fffb32e7d17dc6f7"
+dependencies = [
+ "arrayref",
+ "arrayvec",
+ "cc",
+ "cfg-if",
+ "constant_time_eq",
+ "serde",
+]
+
 [[package]]
 name = "block-buffer"
 version = "0.10.4"
@@ -118,6 +144,15 @@ dependencies = [
  "generic-array",
 ]
 
+[[package]]
+name = "cc"
+version = "1.1.28"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2e80e3b6a3ab07840e1cae9b0666a63970dc28e8ed5ffbcdacbfc760c281bfc1"
+dependencies = [
+ "shlex",
+]
+
 [[package]]
 name = "cfg-if"
 version = "1.0.0"
@@ -170,6 +205,12 @@ version = "1.0.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "0b6a852b24ab71dffc585bcb46eaf7959d175cb865a7152e35b348d1b2960422"
 
+[[package]]
+name = "constant_time_eq"
+version = "0.3.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7c74b8349d32d297c9134b8c88677813a227df8f779daa29bfc29c183fe3dca6"
+
 [[package]]
 name = "cpufeatures"
 version = "0.2.12"
@@ -242,6 +283,7 @@ name = "fayalite"
 version = "0.2.0"
 dependencies = [
  "bitvec",
+ "blake3",
  "clap",
  "eyre",
  "fayalite-proc-macros",
@@ -521,6 +563,12 @@ dependencies = [
  "digest",
 ]
 
+[[package]]
+name = "shlex"
+version = "1.3.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64"
+
 [[package]]
 name = "strsim"
 version = "0.11.1"

Cargo.toml

@@ -19,6 +19,7 @@ fayalite-proc-macros-impl = { version = "=0.2.0", path = "crates/fayalite-proc-m
 fayalite-visit-gen = { version = "=0.2.0", path = "crates/fayalite-visit-gen" }
 base16ct = "0.2.0"
 bitvec = { version = "1.0.1", features = ["serde"] }
+blake3 = { version = "1.5.4", features = ["serde"] }
 clap = { version = "4.5.9", features = ["derive", "env", "string"] }
 eyre = "0.6.12"
 hashbrown = "0.14.3"

crates/fayalite/Cargo.toml

@@ -15,6 +15,7 @@ version.workspace = true
 
 [dependencies]
 bitvec.workspace = true
+blake3.workspace = true
 clap.workspace = true
 eyre.workspace = true
 fayalite-proc-macros.workspace = true

crates/fayalite/src/cli.rs

@@ -12,6 +12,7 @@ use clap::{
     Parser, Subcommand, ValueEnum, ValueHint,
 };
 use eyre::{eyre, Report};
+use serde::{Deserialize, Serialize};
 use std::{
     error,
     ffi::OsString,
@@ -197,8 +198,9 @@ impl BaseArgs {
         &self,
         _acquired_job: &mut AcquiredJob,
         mut command: process::Command,
+        mut captured_output: Option<&mut String>,
     ) -> io::Result<process::ExitStatus> {
-        if self.redirect_output_for_rust_test {
+        if self.redirect_output_for_rust_test || captured_output.is_some() {
             let (reader, writer) = os_pipe::pipe()?;
             let mut reader = io::BufReader::new(reader);
             command.stderr(writer.try_clone()?);
@@ -209,6 +211,9 @@ impl BaseArgs {
             Ok(loop {
                 let status = child.try_wait()?;
                 streaming_read_utf8(&mut reader, |s| {
+                    if let Some(captured_output) = captured_output.as_deref_mut() {
+                        captured_output.push_str(s);
+                    }
                     // use print! so output goes to Rust test output capture
                     print!("{s}");
                     io::Result::Ok(())
@@ -369,6 +374,7 @@ pub struct VerilogArgs {
 pub struct VerilogOutput {
     pub firrtl: FirrtlOutput,
     pub verilog_files: Vec<PathBuf>,
+    pub contents_hash: Option<blake3::Hash>,
 }
 
 impl VerilogOutput {
@@ -386,6 +392,7 @@ impl VerilogArgs {
         let file_separator_prefix = "\n// ----- 8< ----- FILE \"";
         let file_separator_suffix = "\" ----- 8< -----\n\n";
         let mut input = &*input;
+        output.contents_hash = Some(blake3::hash(input.as_bytes()));
         let main_verilog_file = output.main_verilog_file();
         let mut file_name: Option<&Path> = Some(&main_verilog_file);
         loop {
@@ -428,6 +435,7 @@ impl VerilogArgs {
         let output = VerilogOutput {
             firrtl: firrtl_output,
             verilog_files: vec![],
+            contents_hash: None,
         };
         let mut cmd = process::Command::new(firtool);
         cmd.arg(output.firrtl.firrtl_file());
@@ -442,7 +450,7 @@ impl VerilogArgs {
         }
         cmd.args(firtool_extra_args);
         cmd.current_dir(&output.firrtl.output_dir);
-        let status = firrtl.base.run_external_command(acquired_job, cmd)?;
+        let status = firrtl.base.run_external_command(acquired_job, cmd, None)?;
         if status.success() {
             self.process_unadjusted_verilog_file(output)
         } else {
@@ -541,7 +549,7 @@ pub struct FormalArgs {
     )]
     pub sby: PathBuf,
     #[arg(long)]
-    pub sby_extra_args: Vec<OsString>,
+    pub sby_extra_args: Vec<String>,
     #[arg(long, default_value_t)]
     pub mode: FormalMode,
     #[arg(long, default_value_t = Self::DEFAULT_DEPTH)]
@@ -550,6 +558,8 @@ pub struct FormalArgs {
     pub solver: String,
     #[arg(long)]
     pub smtbmc_extra_args: Vec<String>,
+    #[arg(long, default_value_t = true, env = "FAYALITE_CACHE_RESULTS")]
+    pub cache_results: bool,
     #[command(flatten)]
     _formal_adjust_args: FormalAdjustArgs,
 }
@@ -564,16 +574,18 @@ impl fmt::Debug for FormalArgs {
             depth,
             solver,
             smtbmc_extra_args,
+            cache_results,
             _formal_adjust_args: _,
         } = self;
         f.debug_struct("FormalArgs")
-            .field("verilog", &verilog)
-            .field("sby", &sby)
-            .field("sby_extra_args", &sby_extra_args)
-            .field("mode", &mode)
-            .field("depth", &depth)
-            .field("solver", &solver)
-            .field("smtbmc_extra_args", &smtbmc_extra_args)
+            .field("verilog", verilog)
+            .field("sby", sby)
+            .field("sby_extra_args", sby_extra_args)
+            .field("mode", mode)
+            .field("depth", depth)
+            .field("solver", solver)
+            .field("smtbmc_extra_args", smtbmc_extra_args)
+            .field("cache_results", cache_results)
             .finish_non_exhaustive()
     }
 }
@@ -592,6 +604,48 @@ impl FormalOutput {
     pub fn sby_file(&self) -> PathBuf {
         self.verilog.firrtl.file_with_ext("sby")
     }
+    pub fn cache_file(&self) -> PathBuf {
+        self.verilog.firrtl.file_with_ext("cache.json")
+    }
+}
+
+#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
+#[non_exhaustive]
+pub struct FormalCacheOutput {}
+
+#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
+#[non_exhaustive]
+pub enum FormalCacheVersion {
+    V1,
+}
+
+impl FormalCacheVersion {
+    pub const CURRENT: Self = Self::V1;
+}
+
+#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
+#[non_exhaustive]
+pub struct FormalCache {
+    pub version: FormalCacheVersion,
+    pub contents_hash: blake3::Hash,
+    pub stdout_stderr: String,
+    pub result: Result<FormalCacheOutput, String>,
+}
+
+impl FormalCache {
+    pub fn new(
+        version: FormalCacheVersion,
+        contents_hash: blake3::Hash,
+        stdout_stderr: String,
+        result: Result<FormalCacheOutput, String>,
+    ) -> Self {
+        Self {
+            version,
+            contents_hash,
+            stdout_stderr,
+            result,
+        }
+    }
 }
 
 impl FormalArgs {
@@ -604,6 +658,7 @@ impl FormalArgs {
             depth,
             smtbmc_extra_args,
             solver,
+            cache_results: _,
             _formal_adjust_args: _,
         } = self;
         let smtbmc_options = smtbmc_extra_args.join(" ");
@@ -644,7 +699,19 @@ impl FormalArgs {
             verilog: verilog_output,
         };
         let sby_file = output.sby_file();
-        std::fs::write(&sby_file, self.sby_contents(&output)?)?;
+        let sby_contents = self.sby_contents(&output)?;
+        let contents_hash = output.verilog.contents_hash.map(|verilog_hash| {
+            let mut hasher = blake3::Hasher::new();
+            hasher.update(verilog_hash.as_bytes());
+            hasher.update(sby_contents.as_bytes());
+            hasher.update(&(self.sby_extra_args.len() as u64).to_le_bytes());
+            for sby_extra_arg in self.sby_extra_args.iter() {
+                hasher.update(&(sby_extra_arg.len() as u64).to_le_bytes());
+                hasher.update(sby_extra_arg.as_bytes());
+            }
+            hasher.finalize()
+        });
+        std::fs::write(&sby_file, sby_contents)?;
         let mut cmd = process::Command::new(&self.sby);
         cmd.arg("-f");
         cmd.arg(sby_file.file_name().unwrap());
@@ -656,20 +723,62 @@ impl FormalArgs {
             NonZeroUsize::new(1).unwrap()
         };
         let new_minimum_count = AcquiredJob::max_available_job_count().min(new_minimum_count);
+        let mut captured_output = String::new();
+        let cache_file = output.cache_file();
+        let do_cache = if let Some(contents_hash) = contents_hash.filter(|_| self.cache_results) {
+            if let Some(FormalCache {
+                version: FormalCacheVersion::CURRENT,
+                contents_hash: cache_contents_hash,
+                stdout_stderr,
+                result,
+            }) = fs::read(&cache_file)
+                .ok()
+                .and_then(|v| serde_json::from_slice(&v).ok())
+            {
+                if cache_contents_hash == contents_hash {
+                    println!("Using cached formal result:\n{stdout_stderr}");
+                    return match result {
+                        Ok(FormalCacheOutput {}) => Ok(output),
+                        Err(error) => Err(CliError(eyre::Report::msg(error))),
+                    };
+                }
+            }
+            true
+        } else {
+            false
+        };
+        let _ = fs::remove_file(&cache_file);
         let status = acquired_job.increase_job_count(new_minimum_count, |acquired_job| {
-            self.verilog
-                .firrtl
-                .base
-                .run_external_command(acquired_job, cmd)
+            self.verilog.firrtl.base.run_external_command(
+                acquired_job,
+                cmd,
+                do_cache.then_some(&mut captured_output),
+            )
         })?;
-        if status.success() {
+        let result = if status.success() {
             Ok(output)
         } else {
             Err(CliError(eyre!(
                 "running {} failed: {status}",
                 self.sby.display()
             )))
+        };
+        if do_cache {
+            fs::write(
+                cache_file,
+                serde_json::to_string_pretty(&FormalCache {
+                    version: FormalCacheVersion::CURRENT,
+                    contents_hash: contents_hash.unwrap(),
+                    stdout_stderr: captured_output,
+                    result: match &result {
+                        Ok(FormalOutput { verilog: _ }) => Ok(FormalCacheOutput {}),
+                        Err(error) => Err(error.to_string()),
+                    },
+                })
+                .expect("serialization shouldn't ever fail"),
+            )?;
         }
+        result
     }
 }