Desugar: log an (ignorable) error for binder attributes

lib/pulse/lib/Pulse.Lib.HashTable.fst

@@ -45,10 +45,15 @@ let models_timeless #kt #vt (ht:ht_t kt vt) (pht:pht_t kt vt)
   : Lemma (timeless (models ht pht))
           [SMTPat (timeless (models ht pht))] = ()
 
+(* NOTE: We do not add the Rust attributes in these definitions since
+   1- They anyway be ignored by Pulse (currently, should fix)
+   2- The ones that really matter are the ones in the declarations
+      in the fsti (which currently are, and must be, F* vals).
+*)
 
 fn alloc
-  (#[@@@ Rust_generics_bounds ["Copy"; "PartialEq"; "Clone"]] k:eqtype)
-  (#[@@@ Rust_generics_bounds ["Clone"]] v:Type0)
+  (#k:eqtype)
+  (#v:Type0)
   (hashf:(k -> SZ.t)) (l:pos_us)
   requires pure (SZ.fits (2 `op_Multiply` SZ.v l))
   returns ht:ht_t k v
@@ -63,11 +68,9 @@ fn alloc
   ht
 }
 
-
-
 fn dealloc
-  (#[@@@ Rust_generics_bounds ["Copy"; "PartialEq"; "Clone"]] k:eqtype)
-  (#[@@@ Rust_generics_bounds ["Clone"]] v:Type0)
+  (#k:eqtype)
+  (#v:Type0)
   (ht:ht_t k v)
   requires exists* pht. models ht pht
   ensures emp
@@ -85,8 +88,8 @@ let size_t_mod (x:SZ.t) (y : SZ.t { y =!= 0sz })
 #push-options "--fuel 1 --ifuel 1"
 
 fn lookup
-  (#[@@@ Rust_generics_bounds ["Copy"; "PartialEq"; "Clone"]] kt:eqtype)
-  (#[@@@ Rust_generics_bounds ["Clone"]] vt:Type0)
+  (#kt:eqtype)
+  (#vt:Type0)
   (#pht:erased (pht_t kt vt))
   (ht:ht_t kt vt)
   (k:kt)
@@ -200,8 +203,8 @@ fn lookup
 
 
 fn replace
-  (#[@@@ Rust_generics_bounds ["Copy"; "PartialEq"; "Clone"]] kt:eqtype)
-  (#[@@@ Rust_generics_bounds ["Clone"]] vt:Type0)
+  (#kt:eqtype)
+  (#vt:Type0)
   (#pht:erased (pht_t kt vt))
   (ht:ht_t kt vt)
   (idx:SZ.t)
@@ -244,8 +247,8 @@ fn replace
 
 #push-options "--fuel 1 --ifuel 2 --z3rlimit_factor 4"
 fn insert
-  (#[@@@ Rust_generics_bounds ["Copy"; "PartialEq"; "Clone"]] kt:eqtype)
-  (#[@@@ Rust_generics_bounds ["Clone"]] vt:Type0)
+  (#kt:eqtype)
+  (#vt:Type0)
   (ht:ht_t kt vt) (k:kt) (v:vt)
   (#pht:(p:erased (pht_t kt vt){PHT.not_full p.repr}))
   requires models ht pht
@@ -424,8 +427,8 @@ let is_used
 
 
 fn not_full
-  (#[@@@ Rust_generics_bounds ["Copy"; "PartialEq"; "Clone"]] kt:eqtype)
-  (#[@@@ Rust_generics_bounds ["Clone"]] vt:Type0)
+  (#kt:eqtype)
+  (#vt:Type0)
   (ht:ht_t kt vt)
   (#pht:erased (pht_t kt vt))
 
@@ -492,8 +495,8 @@ fn not_full
 
 
 fn insert_if_not_full
-  (#[@@@ Rust_generics_bounds ["Copy"; "PartialEq"; "Clone"]] kt:eqtype)
-  (#[@@@ Rust_generics_bounds ["Clone"]] vt:Type0)
+  (#kt:eqtype)
+  (#vt:Type0)
   (ht:ht_t kt vt) (k:kt) (v:vt)
   (#pht:erased (PHT.pht_t kt vt))
   requires models ht pht
@@ -522,8 +525,8 @@ fn insert_if_not_full
 
 #push-options "--z3rlimit_factor 4"
 fn delete
-  (#[@@@ Rust_generics_bounds ["Copy"; "PartialEq"; "Clone"]] kt:eqtype)
-  (#[@@@ Rust_generics_bounds ["Clone"]] vt:Type0)
+  (#kt:eqtype)
+  (#vt:Type0)
   (ht:ht_t kt vt) (k:kt)
   (#pht:erased (pht_t kt vt))
 

src/syntax_extension/PulseSyntaxExtension.Desugar.fst

@@ -893,6 +893,16 @@ and desugar_binders (env:env_t) (bs:Sugar.binders)
           let rng = b.A.brange in
           let (aq, b, t, attrs) = destruct_binder b in
           let! t = desugar_term env t in
+          if Cons? attrs && not (Options.Ext.enabled "pulse:binder_attrs") then (
+            let open FStarC.Errors.Msg in
+            (* Using "Unused01" error code is a huge hack, but we don't
+            have a way of extending error codes. *)
+            fail_doc [
+              text "NOTE: Pulse does not properly support binder attributes. \
+                    They will be ignored by later stages.";
+              text "This error can be ignored (at your own risk) by passing --ext pulse:binder_attrs."
+            ] (List.hd attrs).range
+          ) else return ();!
           let! attrs = mapM (desugar_term env) attrs in
           let env, bv = push_bv env b in
           let! env, bs, bvs = aux env bs in

src/syntax_extension/PulseSyntaxExtension.Err.fst

@@ -49,8 +49,11 @@ instance err_monad : monad err = {
   ( let! ) = bind_err
 }
 
+let fail_doc #a (message:list Pprint.document) (range:R.range) : err a =
+  fun ctr -> Inr (Some (message, range)), ctr
+
 let fail #a (message:string) (range:R.range) : err a =
-  fun ctr -> Inr (Some (FStarC.Errors.mkmsg message, range)), ctr
+  fail_doc (FStarC.Errors.mkmsg message) range
 
 let fail_if (b:bool) (message:string) (range:R.range) : err unit =
   if b then fail message range else return ()

test/BinderAttrs.fst

@@ -8,6 +8,9 @@ assume
 val f1 ([@@@123] x:int) :
   stt int emp (fun _ -> emp)
 
+(* Binder attrs currently rejected altogether. Ignore that. *)
+#set-options "--ext pulse:binder_attrs"
+
 fn f2 ([@@@123] x:int)
   requires emp
   returns  int

test/nolib/BinderAttrs.fst

@@ -0,0 +1,36 @@
+module BinderAttrs
+
+#lang-pulse
+open Pulse.Nolib
+open FStar.Tactics.V2
+
+assume
+val f1 ([@@@123] x:int) :
+  stt int emp (fun _ -> emp)
+
+fn f2 ([@@@123] x:int)
+  requires emp
+  returns  int
+  ensures  emp
+{ 1 }
+
+(* f1 and f2 should both have the same binder attributes. *)
+
+let typ_of (nm : string) : Tac typ =
+  let tm = pack (Tv_FVar (pack_fv (explode_qn nm))) in
+  tc (cur_env ()) tm
+
+let check (t : typ) : Tac unit =
+  match t with
+  | Tv_Arrow b _c -> (
+    match b.attrs with
+    | [] -> fail "no attrs"
+    | _ -> ()
+  )
+  | _ ->
+    fail "not an arrow"
+
+let _ = assert True by check (typ_of (`%f1))
+
+[@@expect_failure] (* should work, Pulse currently dropping binder attrs *)
+let _ = assert True by check (typ_of (`%f2))