From 6dd87f05a2e41f90421a04506653bf00cc507d09 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Fri, 6 Feb 2026 06:17:23 +0000 Subject: [PATCH 1/2] Opus 4.6 fixes or suppresses a bunch of warnings --- doc/book/code/Alex.fst | 2 ++ doc/book/code/AlexOpaque.fst | 2 ++ doc/book/code/ContextPollution.fst | 3 +++ doc/book/code/Part1.Quicksort.Permutation.fst | 1 + doc/book/code/SMTEncoding.fst | 2 ++ doc/book/code/TypeclassesAlt2.fst | 2 ++ doc/old/tutorial/code/exercises/Ex01a.fst | 2 ++ doc/old/tutorial/code/exercises/Ex10a.fst | 5 +++-- doc/old/tutorial/code/exercises/Ex12.MAC.fst | 4 +++- doc/old/tutorial/code/exercises/Ex12a.ACLs.fst | 2 ++ doc/old/tutorial/code/exercises/Ex12a1.Cap.fst | 4 +++- doc/old/tutorial/code/solutions/Ex12a2.Cap.fst | 6 +++++- doc/old/tutorial/code/solutions/Ex12b.RPC.fst | 13 +++++++++++-- examples/algorithms/GenericStability.fst | 2 +- examples/algorithms/Huffman.fst | 4 ++-- examples/algorithms/IntervalIntersect.fst | 8 ++++---- examples/algorithms/MergeSort2.fst | 4 ++-- examples/crypto/CntProtocol.fst | 10 ++++++++++ examples/crypto/Encrypt_SymEnc.fst | 4 +++- examples/crypto/MAC.fst | 4 +++- examples/crypto/RPC.fst | 10 +++++++++- .../data_structures/BinarySearchTreeFirst.fst | 4 ++-- examples/dependencies/Test.fst | 2 ++ examples/doublylinkedlist/DoublyLinkedList.fst | 16 ++++++++-------- .../doublylinkedlist/DoublyLinkedListIface.fst | 2 +- examples/generic/Interop.fst | 2 +- examples/hello/Hello/Hello.fst | 2 ++ examples/layeredeffects/DM4F_layered5.fst | 2 ++ examples/layeredeffects/GT.fst | 2 ++ examples/layeredeffects/HoareST.fst | 2 ++ examples/layeredeffects/LL.fst | 2 ++ examples/metatheory/LambdaOmega.fst | 10 +++++----- examples/metatheory/StackMachine.fst | 2 +- examples/metatheory/StlcCbvDbParSubst.fst | 6 +++--- examples/metatheory/StlcStrongDbParSubst.fst | 2 +- examples/miniparse/MiniParse.Tac.Impl.fst | 2 ++ examples/native_tactics/Trace.fst | 4 +++- examples/old/StlcCbvDbPntSubstLists.fst | 3 +++ examples/oplss2021/OPLSS2021.IFC.fst | 8 +++++++- examples/printf/SimplePrintfReify.fst | 5 ++++- examples/rel/Benton2004.RHL.fst | 2 +- examples/tactics/Imp.fst | 2 +- examples/tactics/old/ReifiedTc.fst | 2 ++ src/basic/FStarC.Plugins.fst | 1 + src/extraction/FStarC.Extraction.ML.Code.fst | 17 +---------------- src/interactive/FStarC.Interactive.Ide.fst | 3 ++- src/tosyntax/FStarC.ToSyntax.ToSyntax.fst | 6 ++++-- src/typechecker/FStarC.TypeChecker.Err.fst | 1 + .../FStarC.TypeChecker.Generalize.fst | 3 ++- tests/bug-reports/closed/Bug016.fst | 5 +++-- tests/bug-reports/closed/Bug143.fst | 4 +++- tests/bug-reports/closed/Bug2172.fst | 2 ++ tests/bug-reports/closed/Bug2412.fst | 2 ++ tests/bug-reports/closed/Bug262.fst | 4 +++- tests/bug-reports/closed/Bug3865.fst | 2 ++ tests/bug-reports/closed/Bug623.fst | 4 +++- tests/extraction/Div.fst | 2 ++ tests/extraction/Eta_expand.fst | 2 ++ tests/extraction/ExtractAs.fst | 6 ++++++ tests/extraction/Micro.fst | 4 +++- tests/micro-benchmarks/MAC.fst | 2 ++ tests/micro-benchmarks/TestMRef.fst | 4 +++- tests/micro-benchmarks/TestSeq.fst | 2 ++ .../micro-benchmarks/TopLevelIndexedEffects.fst | 4 ++++ tests/micro-benchmarks/TwoPhaseTC.fst | 6 +++--- tests/micro-benchmarks/UseRBMap.fst | 2 ++ tests/micro-benchmarks/UseRBSet.fst | 2 ++ tests/tactics/Div.fst | 2 ++ 68 files changed, 194 insertions(+), 76 deletions(-) diff --git a/doc/book/code/Alex.fst b/doc/book/code/Alex.fst index 0bf3a7558c8..619af31a207 100644 --- a/doc/book/code/Alex.fst +++ b/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 diff --git a/doc/book/code/AlexOpaque.fst b/doc/book/code/AlexOpaque.fst index 09539a8b815..7cc904c3d02 100644 --- a/doc/book/code/AlexOpaque.fst +++ b/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 diff --git a/doc/book/code/ContextPollution.fst b/doc/book/code/ContextPollution.fst index 84282b29f9d..f29e9b78050 100644 --- a/doc/book/code/ContextPollution.fst +++ b/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 diff --git a/doc/book/code/Part1.Quicksort.Permutation.fst b/doc/book/code/Part1.Quicksort.Permutation.fst index f1862f0ea20..8ca8e7c4906 100644 --- a/doc/book/code/Part1.Quicksort.Permutation.fst +++ b/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 diff --git a/doc/book/code/SMTEncoding.fst b/doc/book/code/SMTEncoding.fst index 38542340148..4160297d155 100644 --- a/doc/book/code/SMTEncoding.fst +++ b/doc/book/code/SMTEncoding.fst @@ -13,3 +13,5 @@ let force_a_query = assert (id True) + +#pop-options diff --git a/doc/book/code/TypeclassesAlt2.fst b/doc/book/code/TypeclassesAlt2.fst index 9937230dc2a..cba3ddb63f2 100644 --- a/doc/book/code/TypeclassesAlt2.fst +++ b/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 diff --git a/doc/old/tutorial/code/exercises/Ex01a.fst b/doc/old/tutorial/code/exercises/Ex01a.fst index da458c46d3a..948af6cb7d5 100644 --- a/doc/old/tutorial/code/exercises/Ex01a.fst +++ b/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 \ No newline at end of file diff --git a/doc/old/tutorial/code/exercises/Ex10a.fst b/doc/old/tutorial/code/exercises/Ex10a.fst index da5ce494074..c655c96adf1 100644 --- a/doc/old/tutorial/code/exercises/Ex10a.fst +++ b/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 *) - () - + () \ No newline at end of file diff --git a/doc/old/tutorial/code/exercises/Ex12.MAC.fst b/doc/old/tutorial/code/exercises/Ex12.MAC.fst index 7b0743dc7fd..2e8f57cb242 100644 --- a/doc/old/tutorial/code/exercises/Ex12.MAC.fst +++ b/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') \ No newline at end of file diff --git a/doc/old/tutorial/code/exercises/Ex12a.ACLs.fst b/doc/old/tutorial/code/exercises/Ex12a.ACLs.fst index a93a39cba82..7a1728f1615 100644 --- a/doc/old/tutorial/code/exercises/Ex12a.ACLs.fst +++ b/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 \ No newline at end of file diff --git a/doc/old/tutorial/code/exercises/Ex12a1.Cap.fst b/doc/old/tutorial/code/exercises/Ex12a1.Cap.fst index b66b873785b..c8f018f2d59 100644 --- a/doc/old/tutorial/code/exercises/Ex12a1.Cap.fst +++ b/doc/old/tutorial/code/exercises/Ex12a1.Cap.fst @@ -35,7 +35,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 = MAC.keygen capRead +#pop-options // BEGIN: CapType val issue: f:string{ ACLs.canRead f } -> ML MAC.tag @@ -43,4 +45,4 @@ 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" \ No newline at end of file diff --git a/doc/old/tutorial/code/solutions/Ex12a2.Cap.fst b/doc/old/tutorial/code/solutions/Ex12a2.Cap.fst index b014abf06a3..990bd0d3971 100644 --- a/doc/old/tutorial/code/solutions/Ex12a2.Cap.fst +++ b/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 \ No newline at end of file diff --git a/doc/old/tutorial/code/solutions/Ex12b.RPC.fst b/doc/old/tutorial/code/solutions/Ex12b.RPC.fst index ab8d884cb37..c4d05725cf5 100644 --- a/doc/old/tutorial/code/solutions/Ex12b.RPC.fst +++ b/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 *) \ No newline at end of file diff --git a/examples/algorithms/GenericStability.fst b/examples/algorithms/GenericStability.fst index 5ec4a56ba82..529a08ff314 100644 --- a/examples/algorithms/GenericStability.fst +++ b/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 diff --git a/examples/algorithms/Huffman.fst b/examples/algorithms/Huffman.fst index bf5c9779cad..77519c13dbc 100644 --- a/examples/algorithms/Huffman.fst +++ b/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 diff --git a/examples/algorithms/IntervalIntersect.fst b/examples/algorithms/IntervalIntersect.fst index 32d31578a8d..61b6801f2bf 100644 --- a/examples/algorithms/IntervalIntersect.fst +++ b/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/ -/// +/// \ No newline at end of file diff --git a/examples/algorithms/MergeSort2.fst b/examples/algorithms/MergeSort2.fst index 0958e73f8a7..70a05d8b8d6 100644 --- a/examples/algorithms/MergeSort2.fst +++ b/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 | [] diff --git a/examples/crypto/CntProtocol.fst b/examples/crypto/CntProtocol.fst index d1f56f9a3cd..beb1701aaa9 100644 --- a/examples/crypto/CntProtocol.fst +++ b/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 \ No newline at end of file diff --git a/examples/crypto/Encrypt_SymEnc.fst b/examples/crypto/Encrypt_SymEnc.fst index 97a987c4d61..3dee786d1cc 100644 --- a/examples/crypto/Encrypt_SymEnc.fst +++ b/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 } *) \ No newline at end of file diff --git a/examples/crypto/MAC.fst b/examples/crypto/MAC.fst index 3c3d33cc392..279ce4279ce 100644 --- a/examples/crypto/MAC.fst +++ b/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') \ No newline at end of file diff --git a/examples/crypto/RPC.fst b/examples/crypto/RPC.fst index e71035f3dd8..95e41d3eb9e 100644 --- a/examples/crypto/RPC.fst +++ b/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 *) \ No newline at end of file diff --git a/examples/data_structures/BinarySearchTreeFirst.fst b/examples/data_structures/BinarySearchTreeFirst.fst index f8b51eebf49..74a89abf9ec 100644 --- a/examples/data_structures/BinarySearchTreeFirst.fst +++ b/examples/data_structures/BinarySearchTreeFirst.fst @@ -78,7 +78,7 @@ val index_is_max : #max:int -> x:int -> Lemma (ensures (List.Tot.mem x (in_order_opt t) ==> x <= max)) (decreases t) -let rec index_is_max (#max:int) t x = admit() +let index_is_max (#max:int) t x = admit() (* CH: 2016-07-28 This started failing recently with: ./BinarySearchTreeFirst.fst(91,23-91,24): Subtyping check failed; expected type (x#105346:Prims.int{(Prims.precedes (Prims.LexCons left @@ -98,7 +98,7 @@ val index_is_max2 : #max:int -> x:int -> Lemma (ensures (List.Tot.mem x (in_order_opt t) ==> x <= max)) (decreases t) -let rec index_is_max2 (#max:int) t x = admit() +let index_is_max2 (#max:int) t x = admit() (* CH: 2016-07-28 This started failing recently match t with | None -> () diff --git a/examples/dependencies/Test.fst b/examples/dependencies/Test.fst index c905ee630cd..d416a6b9976 100644 --- a/examples/dependencies/Test.fst +++ b/examples/dependencies/Test.fst @@ -18,4 +18,6 @@ module Test open FStar.IO open Message +#push-options "--warn_error -272" //Warning_TopLevelEffect let main = print_string message +#pop-options \ No newline at end of file diff --git a/examples/doublylinkedlist/DoublyLinkedList.fst b/examples/doublylinkedlist/DoublyLinkedList.fst index 86aac67d093..014d224b6bd 100644 --- a/examples/doublylinkedlist/DoublyLinkedList.fst +++ b/examples/doublylinkedlist/DoublyLinkedList.fst @@ -151,7 +151,7 @@ let piece_ghostly_connections (#t:Type) (p:piece t) : GTot Type0 = | _ -> p.phead == hd nodes /\ p.ptail == last nodes -let rec fragment_ghostly_connections (#t:Type) (f:fragment t) : GTot Type0 = +let fragment_ghostly_connections (#t:Type) (f:fragment t) : GTot Type0 = fragment_for_each0 piece_ghostly_connections f /// Containment properties @@ -163,7 +163,7 @@ let rec nodelist_contained0 (#t:Type) (h0:heap) (nl:nodelist t) : GTot Type0 = match nl with | [] -> True | n :: ns -> h0 `contains` n /\ nodelist_contained0 h0 ns -let rec nodelist_contained (#t:Type) (h0:heap) (nl:nodelist t) : GTot Type0 = +let nodelist_contained (#t:Type) (h0:heap) (nl:nodelist t) : GTot Type0 = nodelist_contained0 h0 nl let dll_contained (#t:Type) (h0:heap) (d:dll t) : GTot Type0 = @@ -176,7 +176,7 @@ let piece_contained (#t:Type) (h0:heap) (p:piece t) : GTot Type0 = h0 `contains` p.ptail /\ nodelist_contained h0 p.pnodes -let rec fragment_contained (#t:Type) (h0:heap) (f:fragment t) : GTot Type0 = +let fragment_contained (#t:Type) (h0:heap) (f:fragment t) : GTot Type0 = fragment_for_each1 piece_contained h0 f /// Footprints @@ -235,7 +235,7 @@ let piece_fp_b (#t:Type) (h0:heap) (p:piece t) : GTot Mod.loc = (Mod.loc_union (Mod.loc_buffer (p.phead@h0).blink) (Mod.loc_buffer (p.ptail@h0).blink)) (nodelist_fp_b h0 p.pnodes) -let rec fragment_fp0 (#t:Type) (f:fragment t) : GTot Mod.loc = +let fragment_fp0 (#t:Type) (f:fragment t) : GTot Mod.loc = match f with | Frag0 -> Mod.loc_none | Frag1 p1 -> piece_fp0 p1 @@ -333,9 +333,9 @@ let dll_aa (#t:Type) (d:dll t) : GTot Type0 = let piece_aa (#t:Type) (p:piece t) : GTot Type0 = nodelist_aa p.pnodes -let rec fragment_aa0 (#t:Type) (f:fragment t) : GTot Type0 = +let fragment_aa0 (#t:Type) (f:fragment t) : GTot Type0 = fragment_for_each0 piece_aa f -let rec fragment_aa_lr (#t:Type) (f:fragment t) : GTot Type0 = +let fragment_aa_lr (#t:Type) (f:fragment t) : GTot Type0 = match f with | Frag0 -> True | Frag1 p1 -> True @@ -372,7 +372,7 @@ let dll_conn (#t:Type) (h0:heap) (d:dll t) : GTot Type0 = let piece_conn (#t:Type) (h0:heap) (p:piece t) : GTot Type0 = nodelist_conn h0 p.pnodes -let rec fragment_conn (#t:Type) (h0:heap) (f:fragment t) : GTot Type0 = +let fragment_conn (#t:Type) (h0:heap) (f:fragment t) : GTot Type0 = fragment_for_each1 piece_conn h0 f /// Validity properties @@ -876,7 +876,7 @@ let piece_merge_fp0 (#t:Type) (h0:heap) /// Fragment merging to a dll -let rec fragment_defragmentable (#t:Type) (h0:heap) (f:fragment t{fragment_valid h0 f}) : +let fragment_defragmentable (#t:Type) (h0:heap) (f:fragment t{fragment_valid h0 f}) : GTot Type0 = let aux (p1 p2:(p:piece t{piece_valid h0 p})) = let a, b = last p1.pnodes, hd p2.pnodes in diff --git a/examples/doublylinkedlist/DoublyLinkedListIface.fst b/examples/doublylinkedlist/DoublyLinkedListIface.fst index 054ea74b413..ee5d69b6c61 100644 --- a/examples/doublylinkedlist/DoublyLinkedListIface.fst +++ b/examples/doublylinkedlist/DoublyLinkedListIface.fst @@ -260,7 +260,7 @@ let rec _lemma_unchanged_node_vals_transitive (h0 h1 h2:HS.mem) (ns:list (node ' | _ :: ns' -> _lemma_unchanged_node_vals_transitive h0 h1 h2 ns' (** Auxiliary predicate: node list is disjoint from region *) -let rec _pred_nl_disjoint (h:HS.mem) (ns:list (node 'a)) = +let _pred_nl_disjoint (h:HS.mem) (ns:list (node 'a)) = DLL.nodelist_fp0 ns `B.loc_disjoint` B.loc_region_only false (HS.get_tip h) (** If [unchanged_node_vals] is true, then it remains true through a push-pop. *) diff --git a/examples/generic/Interop.fst b/examples/generic/Interop.fst index 36a36ac2466..9d9728263ed 100644 --- a/examples/generic/Interop.fst +++ b/examples/generic/Interop.fst @@ -122,7 +122,7 @@ let rec as_lowstar_sig (n:arity{n > 0}) (pre:vale_pre n) (post:vale_post n) : Ty //Avoid some inductive proofs by just letting Z3 unfold the recursive functions above #reset-options "--z3rlimit_factor 10 --max_fuel 5 --initial_fuel 5 --max_ifuel 1 --initial_ifuel 1 --z3cliopt 'smt.qi.eager_threshold=20'" (* wrap v: Turns `v`, a Vale function, into an equivalent a Low* function *) -let rec wrap +let wrap (#n:arity{n > 0}) (#pre:vale_pre n) (#post:vale_post n) diff --git a/examples/hello/Hello/Hello.fst b/examples/hello/Hello/Hello.fst index e71e65a8671..791a69760cb 100644 --- a/examples/hello/Hello/Hello.fst +++ b/examples/hello/Hello/Hello.fst @@ -17,4 +17,6 @@ module Hello open FStar.IO +#push-options "--warn_error -272" //Warning_TopLevelEffect let main = print_string "Hello F*!\n" +#pop-options \ No newline at end of file diff --git a/examples/layeredeffects/DM4F_layered5.fst b/examples/layeredeffects/DM4F_layered5.fst index 494fd78a9be..5273bc30b7d 100644 --- a/examples/layeredeffects/DM4F_layered5.fst +++ b/examples/layeredeffects/DM4F_layered5.fst @@ -142,6 +142,8 @@ let add_via_state (x y : int) : ST int int (fun s0 p -> p (x+y) s0) = put o; r +#push-options "--warn_error -272" //Warning_TopLevelEffect let main = let r, n = reify (reify (add_via_state 1 2) 3) (Ghost.hide (fun _ -> True)) () in FStar.IO.print_string (FStar.Printf.sprintf "%d:%d\n" r n) +#pop-options \ No newline at end of file diff --git a/examples/layeredeffects/GT.fst b/examples/layeredeffects/GT.fst index 529a492b3bb..ae0a73f09c6 100644 --- a/examples/layeredeffects/GT.fst +++ b/examples/layeredeffects/GT.fst @@ -121,3 +121,5 @@ let test #a #i (n:int) : GTD nat i = let r = labs0 n in assume (r >= 0); r + +#pop-options diff --git a/examples/layeredeffects/HoareST.fst b/examples/layeredeffects/HoareST.fst index 45afe3db3dc..f15a6fe1647 100644 --- a/examples/layeredeffects/HoareST.fst +++ b/examples/layeredeffects/HoareST.fst @@ -233,4 +233,6 @@ let copy (#a:Type0) (s:array a) effect HoareSTT (a:Type) (post:post_t a) = HoareST a (fun _ -> True) post +#push-options "--warn_error -272" //Warning_TopLevelEffect let main = FStar.IO.print_string "Hello!" +#pop-options \ No newline at end of file diff --git a/examples/layeredeffects/LL.fst b/examples/layeredeffects/LL.fst index b8ce1471480..65813b3327b 100644 --- a/examples/layeredeffects/LL.fst +++ b/examples/layeredeffects/LL.fst @@ -353,8 +353,10 @@ let test () : Exn int True (fun _ -> True) let test_st () : Pure (option int) True (fun _ -> True) = reify (test ()) () +#push-options "--warn_error -272" //Warning_TopLevelEffect let main = let nopt = test_st () in FStar.IO.print_string (match nopt with | None -> FStar.All.failwith "Unexpected none" | Some n -> FStar.Printf.sprintf "Output: %d\n" n) +#pop-options \ No newline at end of file diff --git a/examples/metatheory/LambdaOmega.fst b/examples/metatheory/LambdaOmega.fst index 95f80590cc8..6e7f59e446e 100644 --- a/examples/metatheory/LambdaOmega.fst +++ b/examples/metatheory/LambdaOmega.fst @@ -558,7 +558,7 @@ let kinding_strengthening_ebnd g x t_x #t #k h = kinding_extensional h g irreducible val kinding_inversion_arrow: #g:env -> #t1:typ -> #t2:typ -> h:(kinding g (TArr t1 t2) KTyp) -> Tot (cand (kinding g t1 KTyp) (kinding g t2 KTyp)) -let rec kinding_inversion_arrow #g #t1 #t2 h = match h with +let kinding_inversion_arrow #g #t1 #t2 h = match h with | KiArr h1 h2 -> Conj h1 h2 irreducible val typing_to_kinding : #g:env -> #e:exp -> #t:typ -> @@ -583,7 +583,7 @@ val tshift_up_above_tsubst_beta : x:var -> t1:typ -> t2:typ -> Lemma (ensures (tshift_up_above x (tsubst_beta t2 t1) = tsubst_beta (tshift_up_above x t2) (tshift_up_above (x + 1) t1))) (decreases t1) -let rec tshift_up_above_tsubst_beta x t1 t2 = +let tshift_up_above_tsubst_beta x t1 t2 = assert(tshift_up_above x (tsubst_beta t2 t1) = tsubst (tsub_inc_above x) (tsubst_beta t2 t1)); @@ -683,7 +683,7 @@ irreducible val typing_substitution: #e:exp -> #v:exp -> #t_x:typ -> h1:(typing g v t_x) -> h2:(typing (extend_evar g 0 t_x) e t) -> Tot (typing g (esubst_beta v e) t) (decreases %[e;h2]) -let rec typing_substitution #e #v #t_x #t #g h1 h2 = +let typing_substitution #e #v #t_x #t #g h1 h2 = let hs : subst_typing (esub_beta v) (extend_evar g 0 t_x) g = fun y hkind -> if y = 0 then h1 else TyVar (y-1) (kinding_extensional hkind g) in @@ -796,7 +796,7 @@ let tsh = tshift_up_above (* shift above and substitute is an identity *) val shift_above_and_subst: s:typ -> y:nat -> t:typ -> Lemma (ensures (ts y t (tsh y s) = s)) (decreases s) -let rec shift_above_and_subst s y t = +let shift_above_and_subst s y t = tsubst_comp (tsub_beta_gen y t) (tsub_inc_above y) s; tsubst_extensional (tsub_comp (tsub_beta_gen y t) (tsub_inc_above y)) tsub_id s; tsubst_id s @@ -813,7 +813,7 @@ val tsubst_commute: t1:typ -> y:nat -> t2:typ -> x:nat{x >= y} -> s:typ -> Lemma (requires True) (ensures (ts x s (ts y t2 t1) = ts y (ts x s t2) (ts (x + 1) (tsh y s) t1))) -let rec tsubst_commute t1 y t2 x s = +let tsubst_commute t1 y t2 x s = tsubst_comp (tsub_beta_gen x s) (tsub_beta_gen y t2) t1; forall_intro (tsubst_commute_aux y x s t2); tsubst_extensional (tsub_comp (tsub_beta_gen x s) (tsub_beta_gen y t2)) diff --git a/examples/metatheory/StackMachine.fst b/examples/metatheory/StackMachine.fst index 6dc9084209d..c31bf0a81da 100644 --- a/examples/metatheory/StackMachine.fst +++ b/examples/metatheory/StackMachine.fst @@ -148,7 +148,7 @@ let rec vstack (ts : tstack) : Type0 = | [] -> unit | t :: ts' -> typeDenote t & vstack ts' -let rec tinstrDenote (#ts:tstack) (#ts':tstack) +let tinstrDenote (#ts:tstack) (#ts':tstack) (i : tinstr ts ts') (s:vstack ts) : Tot (vstack ts') = match i with | TiNConst _ n -> (n, s) diff --git a/examples/metatheory/StlcCbvDbParSubst.fst b/examples/metatheory/StlcCbvDbParSubst.fst index f5ffef3a935..04a80683efc 100644 --- a/examples/metatheory/StlcCbvDbParSubst.fst +++ b/examples/metatheory/StlcCbvDbParSubst.fst @@ -42,7 +42,7 @@ let extend_gen x t g = if x = 0 then extend t g irreducible val weakening : n:nat -> #g:env -> #e:exp -> #t:typ -> t':typ -> h:typing g e t -> Tot (typing (extend_gen n t' g) (shift_up_above n e) t) (decreases h) -let rec weakening n #g #v #t t' h = +let weakening n #g #v #t t' h = let hs : subst_typing (sub_inc_above n) g (extend_gen n t' g) = fun y -> if y < n then TyVar y else TyVar (y+1) in substitution (sub_inc_above n) h hs @@ -205,7 +205,7 @@ let rec subst_below x v s = val subst_closed : v:exp{closed v} -> s:sub -> Lemma (requires True) (ensures (v = subst s v)) (decreases v) -let rec subst_closed v s = subst_below 0 v s +let subst_closed v s = subst_below 0 v s val subst_gen_elam_aux : x:var -> v:exp{closed v} -> y:var -> Lemma (ensures ((sub_elam (sub_beta_gen x v)) y = @@ -274,7 +274,7 @@ val extend_gen_0 : t:typ -> g:env -> let extend_gen_0 t g = forall_intro (extend_gen_0_aux t g) -let rec extend_gen_typing_conversion (#t:typ) (#g:env) (#e0:exp) (#t0:typ) (h:typing (extend t g) e0 t0) +let extend_gen_typing_conversion (#t:typ) (#g:env) (#e0:exp) (#t0:typ) (h:typing (extend t g) e0 t0) :Tot (typing (extend_gen 0 t g) e0 t0) = h val preservation : #e:exp -> #t:typ -> h:typing empty e t{Some? (step e)} -> diff --git a/examples/metatheory/StlcStrongDbParSubst.fst b/examples/metatheory/StlcStrongDbParSubst.fst index 77e6f6aad9c..b3687152f93 100644 --- a/examples/metatheory/StlcStrongDbParSubst.fst +++ b/examples/metatheory/StlcStrongDbParSubst.fst @@ -207,7 +207,7 @@ val substitution_beta : h1:typing g v t_x -> h2:typing (extend t_x g) e t -> Tot (typing g (subst (sub_beta v) e) t) (decreases e) -let rec substitution_beta #e #v #t_x #t #g h1 h2 = +let substitution_beta #e #v #t_x #t #g h1 h2 = let hs : subst_typing (sub_beta v) (extend t_x g) g = fun y -> if y = 0 then h1 else TyVar (y-1) in substitution (sub_beta v) h2 hs diff --git a/examples/miniparse/MiniParse.Tac.Impl.fst b/examples/miniparse/MiniParse.Tac.Impl.fst index 6328caf1677..da16f6d94bf 100644 --- a/examples/miniparse/MiniParse.Tac.Impl.fst +++ b/examples/miniparse/MiniParse.Tac.Impl.fst @@ -307,3 +307,5 @@ let r' : parser_impl r = T.synth_by_tactic (fun () -> gen_parser_impl T.Goal) let j : parser_spec TS.t = TS.package_parser TS.p let j32 : parser_impl j = T.synth_by_tactic (fun () -> gen_parser_impl T.Goal) + +#pop-options diff --git a/examples/native_tactics/Trace.fst b/examples/native_tactics/Trace.fst index 129ea004d9b..bdfc0fca20d 100644 --- a/examples/native_tactics/Trace.fst +++ b/examples/native_tactics/Trace.fst @@ -21,7 +21,7 @@ open FStar.List.Tot (* Do not warn about recursive functions not used in their bodies: since we metaprogram them, the desugaring phase wrongly concludes they do not have to be recursive, but they do. *) -#push-options "--warn_error -328" +#push-options "--warn_error -328" //Warning_UnusedLetRec (* We take a function such as * @@ -194,3 +194,5 @@ let rec fact' (n : nat) (tr : list nat) : Tot (list nat * int) = #pop-options let _ = assert (fact' 5 [] == ([5], 120)) + +#pop-options diff --git a/examples/old/StlcCbvDbPntSubstLists.fst b/examples/old/StlcCbvDbPntSubstLists.fst index 61bb1473b1b..c9326632939 100644 --- a/examples/old/StlcCbvDbPntSubstLists.fst +++ b/examples/old/StlcCbvDbPntSubstLists.fst @@ -301,3 +301,6 @@ let s2 = let test3 = assert (Some? s2 /\ Some?.v s2 = id_app_id)*) *) + +#pop-options +#pop-options diff --git a/examples/oplss2021/OPLSS2021.IFC.fst b/examples/oplss2021/OPLSS2021.IFC.fst index fc6db8bb2cb..34cced8b1aa 100644 --- a/examples/oplss2021/OPLSS2021.IFC.fst +++ b/examples/oplss2021/OPLSS2021.IFC.fst @@ -242,7 +242,7 @@ let has_flow_append (from to:loc) (fs fs':flows) : Lemma (has_flow from to fs ==> has_flow from to (fs @ fs') /\ has_flow from to (fs' @ fs)) - = let rec aux (rs:_) + = let aux (rs:_) : Lemma (requires List.Tot.memP rs fs) (ensures @@ -278,6 +278,7 @@ let rec add_source_monotonic (from to:loc) (r:label) (fs:flows) | [] -> () | _::tl -> add_source_monotonic from to r tl +#push-options "--warn_error -271" //Warning_SMTPatternIllFormed let has_flow_soundness #a #r #w #fs (f:ist a r w fs) (from to:loc) (s:store) (k:int) : Lemma (requires @@ -294,6 +295,7 @@ let has_flow_soundness #a #r #w #fs (f:ist a r w fs) assert (no_leakage f from to) in () +#pop-options let bind_comp_no_leakage (#a #b:Type) (#w0 #r0 #w1 #r1:label) @@ -524,6 +526,7 @@ let subcomp (a:Type) (w0 r0 w1 r1:label) (fs0 fs1:flows) (f:ist a w0 r0 fs0) f /// Package it up as an effect +#push-options "--warn_error -352" //Warning_Adhoc_IndexedEffect_Combinator reflectable layered_effect { IST : a:Type -> @@ -537,6 +540,7 @@ layered_effect { bind = bind; subcomp = subcomp } +#pop-options let read (l:loc) : IST int bot (single l) [] = IST?.reflect (iread l) let write (l:loc) (x:int) : IST unit (single l) bot [] = IST?.reflect (iwrite l x) @@ -544,7 +548,9 @@ let tot a = unit -> Tot a let lift_tot (a:Type) (x:tot a) : ist a bot bot [] = return a (x()) +#push-options "--warn_error -352" //Warning_Adhoc_IndexedEffect_Combinator sub_effect PURE ~> IST = lift_tot +#pop-options //////////////////////////////////////////////////////////////////////////////// // Now for some examples diff --git a/examples/printf/SimplePrintfReify.fst b/examples/printf/SimplePrintfReify.fst index 64972928397..e091384adc2 100644 --- a/examples/printf/SimplePrintfReify.fst +++ b/examples/printf/SimplePrintfReify.fst @@ -17,6 +17,7 @@ module SimplePrintfReify open FStar.Char open FStar.String +open FStar.List.Tot module List = FStar.List.Tot // A variant of SimplePrintf that uses reify on the Ex implementation @@ -45,6 +46,7 @@ let bind_ex a b f g = fun _ -> let raise_ex (_:exn) : Tot (ex False) = fun _ -> None (* Define the new effect using DM4F *) +#push-options "--warn_error -337" //Warning_DeprecatedGeneric total reifiable reflectable new_effect { XEXN : (a:Type) -> Effect with repr = ex @@ -52,6 +54,7 @@ total reifiable reflectable new_effect { ; return = return_ex ; raise = raise_ex } +#pop-options (* A lift from `Pure´ into the new effect *) (* unfold let lift_pure_ex_wp (a:Type) (wp:pure_wp a) (_:unit) (p:XEXN?.post a) = *) @@ -137,7 +140,7 @@ reifiable let rec parse_format (s:list char) : Xex (list dir) = let parse_format_pure (s:list char) : option (list dir) = reify (parse_format s) () -let rec parse_format_string (s:string) : Tot (option (list dir)) = +let parse_format_string (s:string) : Tot (option (list dir)) = parse_format_pure (list_of_string s) let sprintf (s:string{normalize_term #bool (Some? (parse_format_string s))}) diff --git a/examples/rel/Benton2004.RHL.fst b/examples/rel/Benton2004.RHL.fst index 2fe0a9698ca..31e1c2f41d2 100644 --- a/examples/rel/Benton2004.RHL.fst +++ b/examples/rel/Benton2004.RHL.fst @@ -390,7 +390,7 @@ let rec r_while_correct r_while_correct b b' c c' p s1 s1' (fuel - 1) else () -let rec r_while +let r_while (b b' : exp bool) (c c' : computation) (p: gexp bool) diff --git a/examples/tactics/Imp.fst b/examples/tactics/Imp.fst index 7086dde7676..b08b82c4bf5 100644 --- a/examples/tactics/Imp.fst +++ b/examples/tactics/Imp.fst @@ -55,7 +55,7 @@ let override r v rm = then v else rm r' -let rec eval' (i:inst) (rm:regmap) +let eval' (i:inst) (rm:regmap) : Tot regmap (decreases (size i)) = match i with | Add r1 r2 r3 -> override r3 (rm r1 + rm r2) rm diff --git a/examples/tactics/old/ReifiedTc.fst b/examples/tactics/old/ReifiedTc.fst index ee0676afad7..fa838b9ea3e 100644 --- a/examples/tactics/old/ReifiedTc.fst +++ b/examples/tactics/old/ReifiedTc.fst @@ -55,3 +55,5 @@ let test1 = let test2 = assert (set_range_of 1 (range_of 2) === 1) by (apply_lemma (`eq_any)) + +#pop-options diff --git a/src/basic/FStarC.Plugins.fst b/src/basic/FStarC.Plugins.fst index 13b877a8ad1..94ef8710a58 100644 --- a/src/basic/FStarC.Plugins.fst +++ b/src/basic/FStarC.Plugins.fst @@ -24,6 +24,7 @@ open FStarC.Plugins.Base module BU = FStarC.Util module E = FStarC.Errors open FStarC.Class.Show +open FStar.List.Tot let loaded : ref (list string) = mk_ref [] let loaded_plugin_lib : ref bool = mk_ref false diff --git a/src/extraction/FStarC.Extraction.ML.Code.fst b/src/extraction/FStarC.Extraction.ML.Code.fst index f5f9106d82e..fbd95117580 100644 --- a/src/extraction/FStarC.Extraction.ML.Code.fst +++ b/src/extraction/FStarC.Extraction.ML.Code.fst @@ -782,22 +782,7 @@ let doc_of_modbody (currentModule : mlsymbol) (m : mlmodulebody) = reduce (List.flatten docs) (* -------------------------------------------------------------------- *) let doc_of_mlmodule_r (fsharp : bool) (mod : mlmodule) : doc = - let rec p_sig (mod : mlmodule) = - let x, sigmod = mod in - let x = Util.flatten_mlpath x in - let head = reduce1 [text "module"; text x; text ":"; text "sig"] in - let tail = reduce1 [text "end"] in - let doc = Option.map (fun (s, _) -> doc_of_sig x s) sigmod in - - reduce [ - cat head hardline; - (match doc with - | None -> empty - | Some s -> cat s hardline); - cat tail hardline; - ] - - and p_mod istop mod = + let p_mod istop mod = let mod_name, sigmod = mod in let target_mod_name = Util.flatten_mlpath mod_name in let head = reduce1 (if fsharp diff --git a/src/interactive/FStarC.Interactive.Ide.fst b/src/interactive/FStarC.Interactive.Ide.fst index 1eb7b05a6e3..3f466a53f1f 100644 --- a/src/interactive/FStarC.Interactive.Ide.fst +++ b/src/interactive/FStarC.Interactive.Ide.fst @@ -153,7 +153,8 @@ let run_repl_ld_transactions (st: repl_state) (tasks: list repl_task) | [] -> st | (_id, (task, _st')) :: entries -> //NS: this assertion has been failing for a while in debug mode; not sure why - assert (task = fst (snd (List.hd !repl_stack))); + let current_task = fst (snd (List.hd !repl_stack)) in + assert (task = current_task); debug "Reverting" task; let st' = pop_repl "run_repl_ls_transactions" st in let dep_graph = FStarC.TypeChecker.Env.dep_graph st.repl_env in diff --git a/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst b/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst index 6b32e3903f8..36d87c4ed3c 100644 --- a/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst +++ b/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst @@ -506,7 +506,8 @@ let rec desugar_maybe_non_constant_universe t ("Negative universe constant are not supported : " ^ repr); Inl n | Op (op_plus, [t1 ; t2]) -> - assert (Ident.string_of_id op_plus = "+") ; + let op_str = Ident.string_of_id op_plus in + assert (op_str = "+") ; let u1 = desugar_maybe_non_constant_universe t1 in let u2 = desugar_maybe_non_constant_universe t2 in begin match u1, u2 with @@ -524,7 +525,8 @@ let rec desugar_maybe_non_constant_universe t let uarg = desugar_maybe_non_constant_universe targ in aux t (uarg::univargs) | Var max_lid -> - assert (Ident.string_of_lid max_lid = "max") ; + let lid_str = Ident.string_of_lid max_lid in + assert (lid_str = "max") ; if List.existsb (function Inr _ -> true | _ -> false) univargs then Inr (U_max (List.map (function Inl n -> int_to_universe n | Inr u -> u) univargs)) else diff --git a/src/typechecker/FStarC.TypeChecker.Err.fst b/src/typechecker/FStarC.TypeChecker.Err.fst index d07c9fd654d..0ffdbb19d31 100644 --- a/src/typechecker/FStarC.TypeChecker.Err.fst +++ b/src/typechecker/FStarC.TypeChecker.Err.fst @@ -28,6 +28,7 @@ module N = FStarC.TypeChecker.Normalize open FStarC.Errors.Msg open FStarC.Class.Show +open FStar.List.Tot let info_at_pos env file row col : option (either string lident & typ & Range.t) = match TypeChecker.Common.id_info_at_pos !env.identifier_info file row col with diff --git a/src/typechecker/FStarC.TypeChecker.Generalize.fst b/src/typechecker/FStarC.TypeChecker.Generalize.fst index c46ff70262c..14ea2c31e26 100644 --- a/src/typechecker/FStarC.TypeChecker.Generalize.fst +++ b/src/typechecker/FStarC.TypeChecker.Generalize.fst @@ -261,7 +261,8 @@ let gen env (is_rec:bool) (lecs:list (lbname & term & comp)) : option (list (lbn Some ecs let generalize' env (is_rec:bool) (lecs:list (lbname&term&comp)) : (list (lbname&univ_names&term&comp&list binder)) = - assert (List.for_all (fun (l, _, _) -> Inr? l) lecs); //only generalize top-level lets + let all_top = List.for_all (fun (l, _, _) -> Inr? l) lecs in + assert all_top; //only generalize top-level lets if Debug.low () then Format.print1 "Generalizing: %s\n" (show <| List.map (fun (lb, _, _) -> show lb) lecs); diff --git a/tests/bug-reports/closed/Bug016.fst b/tests/bug-reports/closed/Bug016.fst index 3cb68e761bb..602d39380ad 100644 --- a/tests/bug-reports/closed/Bug016.fst +++ b/tests/bug-reports/closed/Bug016.fst @@ -18,9 +18,10 @@ module Bug016 open FStar.All val impossible : u : unit { False } -> Tot 'a +#push-options "--warn_error -272" //Warning_TopLevelEffect let impossible = failwith "this won't happen" +#pop-options val id : 'a -> 'a let id x = x -let three = id 3 - +let three = id 3 \ No newline at end of file diff --git a/tests/bug-reports/closed/Bug143.fst b/tests/bug-reports/closed/Bug143.fst index 6c9f895e0cc..24d245bbada 100644 --- a/tests/bug-reports/closed/Bug143.fst +++ b/tests/bug-reports/closed/Bug143.fst @@ -35,8 +35,10 @@ let delta = Lam f val omega : empty +#push-options "--warn_error -272" //Warning_TopLevelEffect let omega = f delta +#pop-options val bug : unit -> Lemma (requires True) (ensures False) -let bug () = empty_is_empty omega +let bug () = empty_is_empty omega \ No newline at end of file diff --git a/tests/bug-reports/closed/Bug2172.fst b/tests/bug-reports/closed/Bug2172.fst index 3fca4c384ca..88b12ab03f1 100644 --- a/tests/bug-reports/closed/Bug2172.fst +++ b/tests/bug-reports/closed/Bug2172.fst @@ -9,3 +9,5 @@ let p2 = exists (x: int) (y: int). 0 == x + y let test0 (witness:nat) = assert p1 let test1 (x:int) = assert (0 == x + (-x)); assert p2 let _ = assert (p1 <==> p2) + +#pop-options diff --git a/tests/bug-reports/closed/Bug2412.fst b/tests/bug-reports/closed/Bug2412.fst index bcc0aabd59f..a64b93d1680 100644 --- a/tests/bug-reports/closed/Bug2412.fst +++ b/tests/bug-reports/closed/Bug2412.fst @@ -22,4 +22,6 @@ let test _ : ML unit = else () +#push-options "--warn_error -272" //Warning_TopLevelEffect let _ = test() +#pop-options \ No newline at end of file diff --git a/tests/bug-reports/closed/Bug262.fst b/tests/bug-reports/closed/Bug262.fst index 0818c3056ac..f803717a02a 100644 --- a/tests/bug-reports/closed/Bug262.fst +++ b/tests/bug-reports/closed/Bug262.fst @@ -17,12 +17,14 @@ module Bug262 open FStar.ST +#push-options "--warn_error -272" //Warning_TopLevelEffect [@@expect_failure [66]] let log0 = alloc [] val log: ref (list int) //<-- adding this line makes it succeed let log = alloc [] +#pop-options val test : unit -> ST unit (requires (fun h -> Heap.contains h log)) (ensures (fun h0 _ h1 -> Heap.modifies !{log} h0 h1)) -let test () = log := [] +let test () = log := [] \ No newline at end of file diff --git a/tests/bug-reports/closed/Bug3865.fst b/tests/bug-reports/closed/Bug3865.fst index 5a908f2e0c6..cea0eb5e58c 100644 --- a/tests/bug-reports/closed/Bug3865.fst +++ b/tests/bug-reports/closed/Bug3865.fst @@ -14,6 +14,8 @@ let intpak = { f = (fun x -> x + 1); } +#push-options "--warn_error -272" //Warning_TopLevelEffect let use = let x = intpak.f 123 in IO.print_string (string_of_int x ^ "\n") +#pop-options \ No newline at end of file diff --git a/tests/bug-reports/closed/Bug623.fst b/tests/bug-reports/closed/Bug623.fst index 83ff1efecec..a97c5bd6289 100644 --- a/tests/bug-reports/closed/Bug623.fst +++ b/tests/bug-reports/closed/Bug623.fst @@ -22,8 +22,10 @@ val null: unit -> All unit (ensures (fun h r h' -> True)) let null () = () +#push-options "--warn_error -272" //Warning_TopLevelEffect [@@expect_failure [19]] let test0 = assert(false); null () +#pop-options [@@expect_failure [19]] let test1 () = assert(false); null () @@ -57,4 +59,4 @@ val null3: unit -> Pure unit let null3 () = () [@@expect_failure [19]] -let test7 (u:unit) : ML unit = assert(false); null3() +let test7 (u:unit) : ML unit = assert(false); null3() \ No newline at end of file diff --git a/tests/extraction/Div.fst b/tests/extraction/Div.fst index ef5bf840dca..48bc5137b0a 100644 --- a/tests/extraction/Div.fst +++ b/tests/extraction/Div.fst @@ -2,6 +2,8 @@ module Div let rec f () : Dv int = f () +#push-options "--warn_error -272" //Warning_TopLevelEffect let _ = let _ = f () in 1 +#pop-options diff --git a/tests/extraction/Eta_expand.fst b/tests/extraction/Eta_expand.fst index 74a758fd7d7..6c6a45c06a5 100644 --- a/tests/extraction/Eta_expand.fst +++ b/tests/extraction/Eta_expand.fst @@ -34,8 +34,10 @@ let choose: a:t -> dec a -> int -> dec a = function (* One recurring bug has been shadowing of variables when a function is eta-expanded two or more times during extraction. If this is the case, x will be 2 when executing the OCaml code *) +#push-options "--warn_error -272" //Warning_TopLevelEffect let _ = match (choose A 0 2) with | 0 -> () (* correct behaviour *) | 2 -> failwith "Failure of eta-expansion in FStar.Extraction.ML.Term" | _ -> failwith "Unknown failure" +#pop-options \ No newline at end of file diff --git a/tests/extraction/ExtractAs.fst b/tests/extraction/ExtractAs.fst index 11907e2983b..68b510ad121 100644 --- a/tests/extraction/ExtractAs.fst +++ b/tests/extraction/ExtractAs.fst @@ -7,7 +7,9 @@ let fail_unless (b: bool) = if b then "ok" else magic () [@@extract_as (`(fun (x: nat) -> x + 10))] let frob y = 2 + y +#push-options "--warn_error -272" //Warning_TopLevelEffect let _ = fail_unless (frob 1 = 11) +#pop-options // Test that extract_as works when inlining the definition. @@ -15,7 +17,9 @@ inline_for_extraction noextract [@@extract_as (`(fun (x: nat) -> x + 10))] let bar_2 y = 2 + y let bar z = bar_2 z +#push-options "--warn_error -272" //Warning_TopLevelEffect let _ = fail_unless (bar 1 = 11) +#pop-options // It also works if the definition is recursive @@ -23,4 +27,6 @@ let _ = fail_unless (bar 1 = 11) [@@extract_as (`(fun (x: nat) -> x))] let rec loopid (x:nat) : Dv nat = loopid x +#push-options "--warn_error -272" //Warning_TopLevelEffect let two = loopid 2 +#pop-options \ No newline at end of file diff --git a/tests/extraction/Micro.fst b/tests/extraction/Micro.fst index 246b039a94d..6ec88c8f93d 100644 --- a/tests/extraction/Micro.fst +++ b/tests/extraction/Micro.fst @@ -51,7 +51,9 @@ let h6 (s:string) c = c (f6 s) assume val f7: string -> Dv unit +#push-options "--warn_error -272" //Warning_TopLevelEffect let h7:unit = f7 "hello" +#pop-options let g8 (f:int -> 'b) (x:int) : Dv 'b = f x let ignore (x:int) : unit = () @@ -91,4 +93,4 @@ let h12 (n:int) : Dv int = assume val f13 : int -> Dv int let g13 (x:int) : Dv unit = let x = f13 x in - admit() + admit() \ No newline at end of file diff --git a/tests/micro-benchmarks/MAC.fst b/tests/micro-benchmarks/MAC.fst index 82821da4396..d5f5cc17706 100644 --- a/tests/micro-benchmarks/MAC.fst +++ b/tests/micro-benchmarks/MAC.fst @@ -67,7 +67,9 @@ noeq type entry = -> m:tag -> entry +#push-options "--warn_error -272" //Warning_TopLevelEffect let log :ref (list entry) = ST.alloc #(list entry) [] +#pop-options let mac k t = let m = sha1 k t in diff --git a/tests/micro-benchmarks/TestMRef.fst b/tests/micro-benchmarks/TestMRef.fst index 0c512461989..79e659dc3fb 100644 --- a/tests/micro-benchmarks/TestMRef.fst +++ b/tests/micro-benchmarks/TestMRef.fst @@ -20,7 +20,9 @@ open FStar.ST (*assume val x : MRef.mref int increasing *) val x : mref int (fun (x:int) (y:int) -> b2t (y >= x)) +#push-options "--warn_error -272" //Warning_TopLevelEffect let x = alloc 0 +#pop-options assume val y : ref int assume val z : ref int @@ -69,4 +71,4 @@ val test_write_mref : unit -> ST unit (ensures (fun h0 u h1 -> modifies (only x) h0 h1)) let test_write_mref u = let v = read x in - write x (v + 1) + write x (v + 1) \ No newline at end of file diff --git a/tests/micro-benchmarks/TestSeq.fst b/tests/micro-benchmarks/TestSeq.fst index b47b2e655e8..cad66f8acd2 100644 --- a/tests/micro-benchmarks/TestSeq.fst +++ b/tests/micro-benchmarks/TestSeq.fst @@ -26,7 +26,9 @@ let rec print_seq s i = print_string "\n"; print_seq s (i + 1)) +#push-options "--warn_error -272" //Warning_TopLevelEffect let main = let id i = i in let s = Seq.init 10 id in print_seq s 0 +#pop-options \ No newline at end of file diff --git a/tests/micro-benchmarks/TopLevelIndexedEffects.fst b/tests/micro-benchmarks/TopLevelIndexedEffects.fst index 95a0831dde7..1db135e7860 100644 --- a/tests/micro-benchmarks/TopLevelIndexedEffects.fst +++ b/tests/micro-benchmarks/TopLevelIndexedEffects.fst @@ -28,8 +28,10 @@ assume val f (_:unit) : M int // If we try to use this effect at the top-level, F* complains // +#push-options "--warn_error -272" //Warning_TopLevelEffect [@@ expect_failure] let n : int = f () +#pop-options // // We define an identical effect N, @@ -47,4 +49,6 @@ sub_effect PURE ~> N = lift_PURE_M assume val g (_:unit) : N int +#push-options "--warn_error -272" //Warning_TopLevelEffect let n : int = g () +#pop-options \ No newline at end of file diff --git a/tests/micro-benchmarks/TwoPhaseTC.fst b/tests/micro-benchmarks/TwoPhaseTC.fst index 6202c426f84..fcd5212d7bd 100644 --- a/tests/micro-benchmarks/TwoPhaseTC.fst +++ b/tests/micro-benchmarks/TwoPhaseTC.fst @@ -40,7 +40,7 @@ let conjunction_monoid :unit = * This breakage is currently masked by a normalization/compression pass between the two phases. * But we need a better solution. *) -let rec f1: a:Type u#x -> l:list u#x a -> list u#x a = fun a l -> [] +let f1: a:Type u#x -> l:list u#x a -> list u#x a = fun a l -> [] (* * If the recursive let binding (xxx below) is added at different types to Gamma in the two phases, @@ -61,7 +61,7 @@ let rec false_elim (#a:Type) (u:unit{false}) : Tot a = false_elim () let f4 n :nat = 1 let f5 (ls:list nat) :nat = - let rec aux (xs:list nat) :nat = f4 0 + let aux (xs:list nat) :nat = f4 0 in 0 @@ -138,7 +138,7 @@ type solve_1124 (#a:Type) (e1:a) (e2:a): Type = | By: t:unit{e1 == e2} -> solve_1124 e1 e2 val nth_tot_1124: l:list 'a -> n:nat{n < length l} -> Tot 'a -let rec nth_tot_1124 l n = +let nth_tot_1124 l n = match nth l n with | None -> magic() | Some x -> x diff --git a/tests/micro-benchmarks/UseRBMap.fst b/tests/micro-benchmarks/UseRBMap.fst index e52bb0fd625..281287441c7 100644 --- a/tests/micro-benchmarks/UseRBMap.fst +++ b/tests/micro-benchmarks/UseRBMap.fst @@ -3,6 +3,7 @@ module UseRBMap open FStar.RBMap open FStar.Class.Printable +#push-options "--warn_error -272" //Warning_TopLevelEffect let _ = let s = empty () in let s = add 5 "5" s in @@ -22,3 +23,4 @@ let _ = IO.print_string (to_string (lookup 4 s) ^ "\n"); IO.print_string (to_string (lookup 5 s) ^ "\n"); () +#pop-options \ No newline at end of file diff --git a/tests/micro-benchmarks/UseRBSet.fst b/tests/micro-benchmarks/UseRBSet.fst index add9bdb42d0..9431274ec0c 100644 --- a/tests/micro-benchmarks/UseRBSet.fst +++ b/tests/micro-benchmarks/UseRBSet.fst @@ -3,6 +3,7 @@ module UseRBSet open FStar.RBSet open FStar.Class.Printable +#push-options "--warn_error -272" //Warning_TopLevelEffect let _ = let s = empty () in let s = add 5 s in @@ -16,3 +17,4 @@ let _ = IO.print_string (to_string (mem 4 s) ^ "\n"); IO.print_string (to_string (mem 5 s) ^ "\n"); () +#pop-options \ No newline at end of file diff --git a/tests/tactics/Div.fst b/tests/tactics/Div.fst index 2dc0cd48526..2d0117e3e89 100644 --- a/tests/tactics/Div.fst +++ b/tests/tactics/Div.fst @@ -27,4 +27,6 @@ let rec f (x : int) : Dv int = 25 #pop-options let g (x : int) : Tac int = f x +#push-options "--warn_error -272" //Warning_TopLevelEffect let _ = assert True by (let x = g 2 in trivial ()) +#pop-options \ No newline at end of file From 5209f2ee18eb49b8895086ffcbfb5f541d93e334 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Thu, 12 Feb 2026 07:04:23 +0000 Subject: [PATCH 2/2] revert hoisting of terms in asserts --- src/interactive/FStarC.Interactive.Ide.fst | 3 +-- src/tosyntax/FStarC.ToSyntax.ToSyntax.fst | 10 ++++------ src/typechecker/FStarC.TypeChecker.Generalize.fst | 3 +-- 3 files changed, 6 insertions(+), 10 deletions(-) diff --git a/src/interactive/FStarC.Interactive.Ide.fst b/src/interactive/FStarC.Interactive.Ide.fst index 3f466a53f1f..1eb7b05a6e3 100644 --- a/src/interactive/FStarC.Interactive.Ide.fst +++ b/src/interactive/FStarC.Interactive.Ide.fst @@ -153,8 +153,7 @@ let run_repl_ld_transactions (st: repl_state) (tasks: list repl_task) | [] -> st | (_id, (task, _st')) :: entries -> //NS: this assertion has been failing for a while in debug mode; not sure why - let current_task = fst (snd (List.hd !repl_stack)) in - assert (task = current_task); + assert (task = fst (snd (List.hd !repl_stack))); debug "Reverting" task; let st' = pop_repl "run_repl_ls_transactions" st in let dep_graph = FStarC.TypeChecker.Env.dep_graph st.repl_env in diff --git a/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst b/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst index 36d87c4ed3c..8d5ae0c5c05 100644 --- a/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst +++ b/src/tosyntax/FStarC.ToSyntax.ToSyntax.fst @@ -505,9 +505,8 @@ let rec desugar_maybe_non_constant_universe t then raise_error t Errors.Fatal_NegativeUniverseConstFatal_NotSupported ("Negative universe constant are not supported : " ^ repr); Inl n - | Op (op_plus, [t1 ; t2]) -> - let op_str = Ident.string_of_id op_plus in - assert (op_str = "+") ; + | Op (_op_plus, [t1 ; t2]) -> + assert (Ident.string_of_id _op_plus = "+") ; let u1 = desugar_maybe_non_constant_universe t1 in let u2 = desugar_maybe_non_constant_universe t2 in begin match u1, u2 with @@ -524,9 +523,8 @@ let rec desugar_maybe_non_constant_universe t | App(t, targ, _) -> let uarg = desugar_maybe_non_constant_universe targ in aux t (uarg::univargs) - | Var max_lid -> - let lid_str = Ident.string_of_lid max_lid in - assert (lid_str = "max") ; + | Var _max_lid -> + assert (Ident.string_of_lid _max_lid = "max") ; if List.existsb (function Inr _ -> true | _ -> false) univargs then Inr (U_max (List.map (function Inl n -> int_to_universe n | Inr u -> u) univargs)) else diff --git a/src/typechecker/FStarC.TypeChecker.Generalize.fst b/src/typechecker/FStarC.TypeChecker.Generalize.fst index 14ea2c31e26..c46ff70262c 100644 --- a/src/typechecker/FStarC.TypeChecker.Generalize.fst +++ b/src/typechecker/FStarC.TypeChecker.Generalize.fst @@ -261,8 +261,7 @@ let gen env (is_rec:bool) (lecs:list (lbname & term & comp)) : option (list (lbn Some ecs let generalize' env (is_rec:bool) (lecs:list (lbname&term&comp)) : (list (lbname&univ_names&term&comp&list binder)) = - let all_top = List.for_all (fun (l, _, _) -> Inr? l) lecs in - assert all_top; //only generalize top-level lets + assert (List.for_all (fun (l, _, _) -> Inr? l) lecs); //only generalize top-level lets if Debug.low () then Format.print1 "Generalizing: %s\n" (show <| List.map (fun (lb, _, _) -> show lb) lecs);