add crate for external specs

PLSysSec · Jul 22, 2024 · ad49eee · ad49eee
1 parent 1b6579b
commit ad49eee
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 0 deletions.
diff --git a/flux_support/Cargo.toml b/flux_support/Cargo.toml
@@ -0,0 +1,10 @@
+[package]
+name = "flux_support"
+version.workspace = true
+authors.workspace = true
+edition.workspace = true
+
+[package.metadata.flux]
+enabled = true
+
+[dependencies]
diff --git a/flux_support/src/lib.rs b/flux_support/src/lib.rs
@@ -0,0 +1,11 @@
+#[allow(dead_code)]
+#[flux::sig(fn(x: bool[true]))]
+pub fn assert(_x: bool) {}
+
+#[flux::sig(fn(b:bool) ensures b)]
+pub fn assume(b: bool) {
+    if !b {
+        panic!("assume fails")
+    }
+}
+