SSProve backend

cryspen · Nov 15, 2023 · 6f0ace2 · 6f0ace2
1 parent 5d398fe
commit 6f0ace2
Show file tree

Hide file tree

Showing 13 changed files with 3,700 additions and 360 deletions.
diff --git a/cli/options/src/lib.rs b/cli/options/src/lib.rs
@@ -132,6 +132,8 @@ pub enum Backend {
     Fstar(FStarOptions),
     /// Use the Coq backend
     Coq,
+    /// Use the SSProve backend
+    Ssprove,
     /// Use the EasyCrypt backend (warning: work in progress!)
     Easycrypt,
     /// Use the ProVerif backend (warning: work in progress!)
@@ -143,6 +145,7 @@ impl fmt::Display for Backend {
         match self {
             Backend::Fstar(..) => write!(f, "fstar"),
             Backend::Coq => write!(f, "coq"),
+            Backend::Ssprove => write!(f, "ssprove"),
             Backend::Easycrypt => write!(f, "easycrypt"),
             Backend::ProVerif => write!(f, "proverif"),
         }

diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml