Opus 4.6 fixes or suppresses a bunch of warnings

doc/book/code/Alex.fst

@@ -25,3 +25,5 @@ let find_above_for_g (m:nat) : Lemma(exists (i:nat). abs(g i) > m) =
       end 
     end 
   end 
+
+#pop-options

doc/book/code/AlexOpaque.fst

@@ -124,3 +124,5 @@ let find_above_for_g' (m:nat) : Lemma(exists (i:nat). abs(g i) > m) =
     end 
   end 
 //SNIPPET_END: explicit_exists$
+#pop-options
+#pop-options

doc/book/code/ContextPollution.fst

@@ -28,3 +28,6 @@ let test2 (a:Type) (s0 s1 s2: seq a)
   = ()
 //SNIPPET_END: using_facts$  
 
+
+#pop-options
+#pop-options

doc/book/code/Part1.Quicksort.Permutation.fst

@@ -142,3 +142,4 @@ let rec sort_intrinsic (#a:eqtype) (f:total_order_t a) (l:list a)
       append (sort_intrinsic f lo) (pivot :: sort_intrinsic f hi)
 
 
+#pop-options

doc/book/code/SMTEncoding.fst

@@ -13,3 +13,5 @@ let force_a_query = assert (id True)
 
 
 
+
+#pop-options

doc/book/code/TypeclassesAlt2.fst

@@ -235,3 +235,5 @@ instance __base_comp #a {| d : bounded_unsigned_int_ops a |}
 let try_sub3 {| bounded_unsigned_int_ops 'a |}
              (acc:'a)
   = bound `sub` acc
+
+#pop-options

doc/old/tutorial/code/exercises/Ex01a.fst

@@ -82,4 +82,6 @@ let dynamicChecking () =
   checkedWrite passwd "junk" (* this raises exception *)
 // END: DynamicChecking
 
+#push-options "--warn_error -272" //Warning_TopLevelEffect
 let main = staticChecking (); dynamicChecking ()
+#pop-options

doc/old/tutorial/code/exercises/Ex10a.fst

@@ -36,7 +36,9 @@ let canRead db file =
 
 (* The acls reference stores the current access-control list, initially empty *)
 val acls: ref db
+#push-options "--warn_error -272" //Warning_TopLevelEffect
 let acls = ST.alloc []
+#pop-options
 
 (*
    Here are two stateful functions which alter the access control list.
@@ -109,5 +111,4 @@ let test_acls f =
   safe_delete f;          (* ok, but fails dynamically *)
   revoke (Readable f);
   //let _ = read f in       (* not ok any more *) 
-  ()
-
+  ()

doc/old/tutorial/code/exercises/Ex12.MAC.fst

@@ -53,7 +53,9 @@ type entry =
 
 
 private type log_t = ref (list entry)
+#push-options "--warn_error -272" //Warning_TopLevelEffect
 let log:log_t = ST.alloc #(list entry) []
+#pop-options
 
 // BEGIN: MacSpec
 val keygen: p:(text -> Type) -> ML (pkey p)
@@ -101,4 +103,4 @@ let verify k text tag =
 (* VARIANT CTXT vs CPA: is the tag authenticated?
    otherwise do not include m:tag in the entry *)
 
-//      (fun (Entry k' text' tag') -> k=k' && text=text' && tag=tag')
+//      (fun (Entry k' text' tag') -> k=k' && text=text' && tag=tag')

doc/old/tutorial/code/exercises/Ex12a.ACLs.fst

@@ -71,4 +71,6 @@ let dynamicChecking () =
   checkedWrite tmp "hello!";
   checkedWrite passwd "junk" (* this raises exception *)
 
+#push-options "--warn_error -272" //Warning_TopLevelEffect
 let main = staticChecking (); dynamicChecking ()
+#pop-options

doc/old/tutorial/code/exercises/Ex12a1.Cap.fst

@@ -35,12 +35,14 @@ assume UTF8_inj:
 
 type capRead (msg:bytes) = (forall f. msg = utf8 f ==> ACLs.canRead f)
 
+#push-options "--warn_error -272" //Warning_TopLevelEffect
 let k = MAC.keygen capRead
+#pop-options
 
 // BEGIN: CapType
 val issue: f:string{ ACLs.canRead f } -> ML MAC.tag
 val redeem: f:string -> m:MAC.tag -> ML (u:unit{ ACLs.canRead f })
 // END: CapType
 
 let issue f = failwith "Implement this function"
-let redeem f t = failwith "Implement this function"
+let redeem f t = failwith "Implement this function"

doc/old/tutorial/code/solutions/Ex12a2.Cap.fst

@@ -33,7 +33,9 @@ assume UTF8_inj:
 
 type capRead (msg:bytes) = (forall f. msg = utf8 f ==> ACLs.canRead f)
 
+#push-options "--warn_error -272" //Warning_TopLevelEffect
 let k_read = MAC.keygen capRead
+#pop-options
 
 val issue_read: f:string{ ACLs.canRead f } -> ML MAC.tag
 val redeem_read: f:string -> m:MAC.tag -> ML (u:unit{ ACLs.canRead f })
@@ -55,7 +57,9 @@ let redeem_read f t =
 // Begin: CapImplementation2
 type capWrite (msg:bytes) = (forall f. msg = utf8 f ==> ACLs.canWrite f)
 
+#push-options "--warn_error -272" //Warning_TopLevelEffect
 let k_write = MAC.keygen capWrite
+#pop-options
 
 val issue_write: f:string{ ACLs.canWrite f } -> ML MAC.tag
 val redeem_write: f:string -> m:MAC.tag -> ML(u:unit{ ACLs.canWrite f })
@@ -74,4 +78,4 @@ let redeem_write f t =
     assert(ACLs.canWrite f))
   else
     failwith "bad capability"
-// END: CapImplementation2
+// END: CapImplementation2

doc/old/tutorial/code/solutions/Ex12b.RPC.fst

@@ -26,8 +26,9 @@ open FStar.MRef
 open FStar.List.Tot
 open FStar.String
 
-
+#push-options "--warn_error -272" //Warning_TopLevelEffect
 let init_print = print_string "\ninitializing...\n\n"
+#pop-options
 
 open Platform.Bytes
 open Ex12.SHA1
@@ -39,7 +40,9 @@ module Formatting = Ex12b2.Format
 
 (** some basic, untrusted network controlled by the adversary *)
 val msg_buffer: ref message
+#push-options "--warn_error -272" //Warning_TopLevelEffect
 let msg_buffer = alloc (empty_bytes)
+#pop-options
 
 // BEGIN: Network
 private val send: message -> St unit
@@ -68,7 +71,9 @@ let subset (#a:eqtype) : Tot (preorder (list a)) = subset'
 
 type lref = mref (list log_entry) subset
 
+#push-options "--warn_error -272" //Warning_TopLevelEffect
 private let log : lref = alloc #_ #(subset #log_entry) []
+#pop-options
 
 let add_to_log (r:lref) (v:log_entry) :
       ST unit (requires (fun _ -> True))
@@ -97,8 +102,10 @@ type reqresp text =
 // END: MsgProperty
 
 val k:pkey reqresp
+#push-options "--warn_error -272" //Warning_TopLevelEffect
 let k = print_string "generating shared key...\n";
   keygen reqresp
+#pop-options
 
 
 val client_send : s:string16 -> ML unit
@@ -178,5 +185,7 @@ let test () =
     print_string "\n\n"
 
 val run : unit
+#push-options "--warn_error -272" //Warning_TopLevelEffect
 let run = test ()
-(* check_marker *)
+#pop-options
+(* check_marker *)

examples/algorithms/GenericStability.fst

@@ -120,7 +120,7 @@ val stable_append_r: #a:eqtype ->
   k:(a -> Tot int) ->
   Lemma (requires (stable l l' k))
         (ensures(stable (l@r) (l'@r) k))
-let rec stable_append_r #a l l' r k =
+let stable_append_r #a l l' r k =
   filter_eq_append l r k;
   filter_eq_append l' r k
 

examples/algorithms/Huffman.fst

@@ -197,7 +197,7 @@ let rec decode_prefix_aux (t':trie{Node? t'}) (t:trie)
   | Node _ t1 t2, b::bs'' ->
       decode_prefix_aux t' (if b then t2 else t1) bs'' bs' s
 
-let rec decode_prefix (t:trie{Node? t})
+let decode_prefix (t:trie{Node? t})
   (bs:list bool) (bs':list bool{Cons? bs'}) (s:symbol) : Lemma
   (requires (decode t bs = Some [s]))
   (ensures (decode t (bs @ bs') = (match decode t bs' with
@@ -222,7 +222,7 @@ let rec cancelation_aux (t:trie{Node? t}) (ss:list symbol) : Lemma
     | Some bs, Some bs' -> decode_prefix t bs bs' s
     | _, _ -> ())
 
-let rec cancelation (sws:list (symbol&pos)) (ss:list symbol) : Lemma
+let cancelation (sws:list (symbol&pos)) (ss:list symbol) : Lemma
   (requires (b2t (List.Tot.length sws > 1)))
   (ensures (List.Tot.length sws > 1 ==>
             (let t = huffman sws in

examples/algorithms/IntervalIntersect.fst

@@ -419,7 +419,7 @@ let lemma_subset_prefix (is1:intervals{Cons? is1}) (is2:intervals{Cons? is2})
 /// proof. The other was the importance of set operation distributivity for the
 /// proof.
 
-let rec lemma_overlapping_prefix (is1:intervals{Cons? is1}) (is2:intervals{Cons? is2})
+let lemma_overlapping_prefix (is1:intervals{Cons? is1}) (is2:intervals{Cons? is2})
   : Lemma
     (requires (hd is1).to >^ (hd is2).to /\ (hd is1).from <^ (hd is2).to)
     (ensures (
@@ -511,8 +511,6 @@ let rec lemma_intersection_spec (is1:intervals) (is2:intervals)
 
 /// The following pragma resets the SMT solver to its original resource limit (roughly 5 seconds):
 
-  #reset-options
-
 /// Taking stock: intrinsic vs. extrinsic, intensional vs extensional
 /// -----------------------------------------------------------------
 ///
@@ -590,10 +588,12 @@ let rec ppIntervals' (is:intervals): ML unit =
 let toI f t = I (int_to_t f) (int_to_t t)
 
 let ppIntervals is : ML string = FStar.List.Tot.fold_left (sprintf "%s %s") "" (FStar.List.map ppInterval is)
+#push-options "--warn_error -272" //Warning_TopLevelEffect
 let main =
   print_string
     (ppIntervals (intersect [toI 3 10; toI 10 15] [toI 1 4; toI 10 14]));
   print_newline ()
+#pop-options
 
 /// And the winner is!
 /// ==================
@@ -681,4 +681,4 @@ let main =
 ///
 /// .. _`Jonathan Protzenko`: https://jonathan.protzenko.fr/
 /// .. _KaraMeL: https://github.com/FStarLang/karamel/
-/// 
+/// 

examples/algorithms/MergeSort2.fst

@@ -106,11 +106,11 @@ let rec split_n #a l n =
 
 (** split_half splits a list halfway **)
 val split_half: #a:eqtype -> (l:list a{length l >= 2}) ->
-  Tot (l_tup:(list a & list a))
+  Tot (list a & list a)
 let split_half #a l = split_n l ((length l) / 2)
 
 (** Define mergesort **)
-val mergesort': #a:eqtype -> l:list a -> k:(a -> Tot int) -> Tot (l':list a) (decreases (length l))
+val mergesort': #a:eqtype -> l:list a -> k:(a -> Tot int) -> Tot (list a) (decreases (length l))
 let rec mergesort' #a l k =
   match l with
   | []

examples/crypto/CntProtocol.fst

@@ -9,7 +9,9 @@ open FStar.String
 open FStar.IO
 open FStar.Ref
 
+#push-options "--warn_error -272" //Warning_TopLevelEffect
 let init_print = print_string "\ninitializing...\n\n"
+#pop-options
 
 open Platform.Bytes
 open SHA1
@@ -24,6 +26,7 @@ let max x y = if x > y then x else y
 type event =
   | Recv : m:uint32 -> c:uint16 -> event
 
+#push-options "--warn_error -272" //Warning_TopLevelEffect
 val log_prot: ref (list event)
 let log_prot = ST.alloc []
 
@@ -32,6 +35,7 @@ let client_cnt = lemma_repr_bytes_values 1; ST.alloc 1
 
 val server_cnt: ref uint16
 let server_cnt = lemma_repr_bytes_values 0; ST.alloc 0
+#pop-options
 
 val server_max: l:list event -> Tot (uint16)
 let rec server_max l =
@@ -105,8 +109,10 @@ let log_and_update s c =
 
 (* some basic, untrusted network controlled by the adversary *)
 
+#push-options "--warn_error -272" //Warning_TopLevelEffect
 val msg_buffer: ref message
 let msg_buffer = ST.alloc (empty_bytes)
+#pop-options
 
 val send: message -> ST unit
 		       (requires (fun h -> True))
@@ -132,8 +138,10 @@ assume type signal : uint32 -> uint16 -> Type
 type req (msg:message) =
     (exists s c.   msg = CntFormat.signal s c /\ signal s c)
 
+#push-options "--warn_error -272" //Warning_TopLevelEffect
 val k: k:key{key_prop k == req}
 let k = keygen req
+#pop-options
 
 let recall_all () :ST unit (requires (fun h0      -> True))
                            (ensures  (fun h0 _ h1 -> h0 == h1     /\
@@ -177,6 +185,7 @@ let server () =
 	) else Some "Counter already used"
     ) else Some "Wrong length")
 
+#push-options "--warn_error -272" //Warning_TopLevelEffect
 let main =
   let x = 10 in
   lemma_repr_bytes_values x;
@@ -194,3 +203,4 @@ let main =
     | None -> print_string "Success!\n"
     | Some x -> print_string ("Failure : "^x^"\n")
   end
+#pop-options

examples/crypto/Encrypt_SymEnc.fst

@@ -46,7 +46,9 @@ val encrypt: #p:Type0 -> k:key p AES.plain -> plain: p -> ML (cipher p AES.plain
 
 (* TODO: implementation *)
 
+#push-options "--warn_error -272" //Warning_TopLevelEffect
 let c :ref nat = ST.alloc 0
+#pop-options
 
 let keygen #p safe plain repr =
   let i = !c in
@@ -88,4 +90,4 @@ let decrypt #p k c =
 (* (\* for CPA, ciphers should not be forgeable, but we need to be able to treat sbytes as cipher after checking e.g. a MAC *\) *)
 
 (* assume val decrypt: p:Type -> r:Type -> k:skey p r -> c: cipher p r k -> option p  *)
-(* assume val encrypt: p:Type -> r:Type -> k:skey p r -> plain: p -> c:cipher p r k { decrypt p r k c = plain } *)
+(* assume val encrypt: p:Type -> r:Type -> k:skey p r -> plain: p -> c:cipher p r k { decrypt p r k c = plain } *)

examples/crypto/MAC.fst

@@ -42,7 +42,9 @@ type entry =
          -> m:tag
          -> entry
 
+#push-options "--warn_error -272" //Warning_TopLevelEffect
 let log :ref (list entry) = ST.alloc #(list entry) []
+#pop-options
 
 val keygen: p:(text -> Type) -> St (pkey p)
 val mac:    k:key -> t:text{key_prop k t} -> ST tag 
@@ -105,4 +107,4 @@ let verify k text tag =
 (* VARIANT CTXT vs CPA: is the tag authenticated?
    otherwise do not include m:tag in the entry *)
 
-//      (fun (Entry k' text' tag') -> k=k' && text=text' && tag=tag')
+//      (fun (Entry k' text' tag') -> k=k' && text=text' && tag=tag')

examples/crypto/RPC.fst

@@ -6,7 +6,9 @@ open FStar.All
 open FStar.String
 open FStar.IO
 
+#push-options "--warn_error -272" //Warning_TopLevelEffect
 let init_print = print_string "\ninitializing...\n\n"
+#pop-options
 
 open Platform.Bytes
 (*open Seq
@@ -20,7 +22,9 @@ open MAC
 
 (*let log_prot = ST.alloc []*)
 val msg_buffer: ref message
+#push-options "--warn_error -272" //Warning_TopLevelEffect
 let msg_buffer = ST.alloc (empty_bytes)
+#pop-options
 
 val send: message -> ML unit
 let send m = msg_buffer := m
@@ -45,8 +49,10 @@ type reqresp (msg:message) =
 
 (* FIXME: this type annotation is a workaround for #486 *)
 val k: k:key{key_prop k == reqresp}
+#push-options "--warn_error -272" //Warning_TopLevelEffect
 let k = print_string "generating shared key...\n";
   keygen reqresp
+#pop-options
 
 
 val client_send : string16 -> ML unit
@@ -113,5 +119,7 @@ let test () =
     print_string "\n\n"
 
 val run : unit
+#push-options "--warn_error -272" //Warning_TopLevelEffect
 let run = test ()
-(* check_marker *)
+#pop-options
+(* check_marker *)