Merge pull request #846 from hacspec/fix-fsti-fst-options

F*: macros: make `verification_status` and `options` appear in impl not interfaces

engine/backends/fstar/fstar_backend.ml

@@ -1463,15 +1463,13 @@ struct
           |> Option.value_or_thunk ~default:(fun _ ->
                  Error.assertion_failure e.span
                    "Malformed `Quote` item: could not find a ItemQuote payload")
-          |> Option.value ~default:Types.{ intf = true; impl = false }
+          |> Option.value ~default:Types.{ intf = false; impl = true }
         in
-        (if fstar_opts.intf then
-         [ `VerbatimIntf (pquote e.span quote, `Newline) ]
-        else [])
-        @
-        if fstar_opts.impl then
-          [ `VerbatimImpl (pquote e.span quote, `Newline) ]
-        else []
+        let payload = (pquote e.span quote, `Newline) in
+        if ctx.interface_mode then
+          (if fstar_opts.intf then [ `VerbatimIntf payload ] else [])
+          @ if fstar_opts.impl then [ `VerbatimImpl payload ] else []
+        else [ `VerbatimImpl payload ]
     | HaxError details ->
         [
           `Comment
@@ -1628,8 +1626,12 @@ let string_of_items ~signature_only ~mod_name (bo : BackendOptions.t) m items :
     in
     match lines with [] -> "" | _ -> header ^ String.concat ~sep:"\n" lines
   in
-  ( string_for (function `Impl s -> Some s | _ -> None),
-    string_for (function `Intf s -> Some s | _ -> None) )
+  let replace =
+    String.substr_replace_all ~pattern:"_hax_panic_freedom_admit_"
+      ~with_:"admit () (* Panic freedom *)"
+  in
+  ( string_for (function `Impl s -> Some (replace s) | _ -> None),
+    string_for (function `Intf s -> Some (replace s) | _ -> None) )
 
 let fstar_headers (bo : BackendOptions.t) =
   let opts =

hax-lib-macros/src/lib.rs

@@ -68,14 +68,14 @@ pub fn fstar_verification_status(attr: pm::TokenStream, item: pm::TokenStream) -
                 **last = syn::Stmt::Expr(
                     parse_quote! {
                         {let result = #last;
-                        ::hax_lib::fstar!("admit()");
+                        ::hax_lib::fstar!("_hax_panic_freedom_admit_");
                          result}
                     },
                     None,
                 );
             } else {
                 item.block.stmts.push(syn::Stmt::Expr(
-                    parse_quote! {::hax_lib::fstar!("admit()")},
+                    parse_quote! {::hax_lib::fstar!("_hax_panic_freedom_admit_")},
                     None,
                 ));
             }

test-harness/src/snapshots/toolchain__attributes into-fstar.snap

@@ -317,6 +317,43 @@ let double (x: u8) : Prims.Pure t_Even (requires x <. 127uy) (fun _ -> Prims.l_T
 let double_refine (x: u8) : Prims.Pure t_Even (requires x <. 127uy) (fun _ -> Prims.l_True) =
   x +! x <: t_Even
 '''
+"Attributes.Verifcation_status.fst" = '''
+module Attributes.Verifcation_status
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+let a_panicfree_function (_: Prims.unit)
+    : Prims.Pure u8
+      Prims.l_True
+      (ensures
+        fun x ->
+          let x:u8 = x in
+          false) =
+  let a:u8 = 3uy in
+  let b:u8 = 6uy in
+  let result:u8 = a +! b in
+  let _:Prims.unit = admit () (* Panic freedom *) in
+  result
+
+let another_panicfree_function (_: Prims.unit)
+    : Prims.Pure Prims.unit
+      Prims.l_True
+      (ensures
+        fun x ->
+          let x:Prims.unit = x in
+          false) =
+  let not_much:i32 = 0l in
+  let nothing:i32 = 0l in
+  let still_not_much:i32 = not_much +! nothing in
+  admit () (* Panic freedom *)
+
+#push-options "--admit_smt_queries true"
+
+let a_function_which_only_laxes (_: Prims.unit) : Prims.unit = Hax_lib.v_assert false
+
+#pop-options
+'''
 "Attributes.fst" = '''
 module Attributes
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"

tests/attributes/src/lib.rs

@@ -300,3 +300,26 @@ mod inlined_code_ensures_requires {
         v[3] += 1;
     }
 }
+
+mod verifcation_status {
+    #[hax_lib::fstar::verification_status(lax)]
+    fn a_function_which_only_laxes() {
+        assert!(/*very complicated stuff*/ false)
+    }
+
+    #[hax_lib::fstar::verification_status(panic_free)]
+    #[hax_lib::ensures(|x|/*very complicated stuff*/false)]
+    fn a_panicfree_function() -> u8 {
+        let a = 3;
+        let b = 6;
+        a + b
+    }
+
+    #[hax_lib::fstar::verification_status(panic_free)]
+    #[hax_lib::ensures(|x|/*very complicated stuff*/false)]
+    fn another_panicfree_function() {
+        let not_much = 0;
+        let nothing = 0;
+        let still_not_much = not_much + nothing;
+    }
+}