Run `.scripts/remove_all_unused_opens.sh src/ ulib/ doc/ tests/ examp…

…les/ contrib/`
FStarLang · Feb 14, 2025 · 9b7eb79 · 9b7eb79
1 parent 69287dd
commit 9b7eb79
Show file tree

Hide file tree

Showing 162 changed files with 0 additions and 288 deletions.
diff --git a/contrib/CoreCrypto/ml/Tests.ml b/contrib/CoreCrypto/ml/Tests.ml
@@ -1,6 +1,3 @@
-(* The original "Bytes" module from OCaml. *)
-module B = Bytes
-
 (* This brings [Platform.Bytes] into scope. *)
 open CoreCrypto
 open Platform

diff --git a/doc/book/code/ContextPollution.fst b/doc/book/code/ContextPollution.fst
@@ -3,9 +3,6 @@ module ContextPollution
 let warmup (x:bool { x == true }) = assert x
 
 //SNIPPET_START: context_test1$
-module T = FStar.Tactics
-module B = LowStar.Buffer
-module SA = Steel.Array
 open FStar.Seq
 
 #push-options "--query_stats"

diff --git a/doc/book/code/exercises/Part3.Typeclasses.fst b/doc/book/code/exercises/Part3.Typeclasses.fst
@@ -1,5 +1,4 @@
 module Part3.Typeclasses
-module TC = FStar.Tactics.Typeclasses
 
 class printable (a:Type) =
 {

diff --git a/doc/old/tutorial/code/exercises/LowStar.Ex3.fst b/doc/old/tutorial/code/exercises/LowStar.Ex3.fst
@@ -27,9 +27,6 @@ open FStar.Integers
 /// we don't end up referring to FStar.ST by accident.
 module B = LowStar.Buffer
 module HS = FStar.HyperStack
-module M = LowStar.Modifies
-module ST = FStar.HyperStack.ST
-module S = FStar.Seq
 
 /// This brings into scope the ``!*`` and ``*=`` operators, which are
 /// specifically designed to operate on buffers of size 1, i.e. on pointers.

diff --git a/doc/old/tutorial/code/solutions/Ex12a1.Cap.fst b/doc/old/tutorial/code/solutions/Ex12a1.Cap.fst
@@ -23,7 +23,6 @@ open Platform.Bytes
 
 module ACLs = Ex12a.ACLs
 module MAC = Ex12.MAC
-module SHA1 = Ex12.SHA1
 
 // In Platform.Bytes: val utf8: s:string  -> Tot bytes
 

diff --git a/doc/old/tutorial/code/solutions/LowStar.Ex3.fst b/doc/old/tutorial/code/solutions/LowStar.Ex3.fst
@@ -24,8 +24,6 @@ open FStar.Integers
 module B = LowStar.Buffer
 module HS = FStar.HyperStack
 module M = LowStar.Modifies
-module ST = FStar.HyperStack.ST
-module S = FStar.Seq
 
 /// This brings into scope the ``!*`` and ``*=`` operators, which are
 /// specifically designed to operate on buffers of size 1, i.e. on pointers.

diff --git a/examples/crypto/HyE.AE.fst b/examples/crypto/HyE.AE.fst
@@ -26,7 +26,6 @@ module CC = CoreCrypto
 module B = Platform.Bytes
 
 open HyE.Plain
-module Plain = HyE.Plain
 
 noeq type key : Type0 =
   | Key: #region:erid -> raw:aes_key -> log:mlog_t region -> key

diff --git a/examples/crypto/HyE.AE.fsti b/examples/crypto/HyE.AE.fsti
@@ -22,7 +22,6 @@ open HyE.Ideal
 
 open Platform.Bytes
 open CoreCrypto
-module CC = CoreCrypto
 module B = Platform.Bytes
 
 open HyE.Plain

diff --git a/examples/crypto/HyE.HCCA2.fst b/examples/crypto/HyE.HCCA2.fst
@@ -21,8 +21,6 @@ open HyE.PlainPKE
 open Platform.Bytes
 open FStar.HyperStack
 
-module B = Platform.Bytes
-module P = HyE.Plain
 module C = HyE.CCA2
 module A = HyE.AE
 module RSA = HyE.RSA

diff --git a/examples/crypto/HyE.HCCA2.fsti b/examples/crypto/HyE.HCCA2.fsti
@@ -21,7 +21,6 @@ open HyE.PlainPKE
 open Platform.Bytes
 open FStar.HyperStack
 
-module B = Platform.Bytes
 module P = HyE.Plain
 module C = HyE.CCA2
 module A = HyE.AE

diff --git a/examples/crypto/HyE.RSA.fst b/examples/crypto/HyE.RSA.fst
@@ -32,7 +32,6 @@ open FStar.List.Tot
 open Platform.Bytes
 open CoreCrypto
 
-module B = Platform.Bytes
 
 assume type pkey
 assume type skey

diff --git a/examples/crypto/OPLSS.Log.fst b/examples/crypto/OPLSS.Log.fst
@@ -6,7 +6,6 @@ open FStar.HyperStack
 module HS = FStar.HyperStack
 module HST = FStar.HyperStack.ST
 module B = LowStar.Monotonic.Buffer
-module L = FStar.List.Tot
 
 let grows (#a:Type)
   : Preorder.preorder (seq a)

diff --git a/examples/crypto/OPLSS.fst b/examples/crypto/OPLSS.fst
@@ -1,8 +1,5 @@
 module OPLSS
 module UInt8 = FStar.UInt8
-module HS = FStar.HyperStack
-module ST = FStar.HyperStack.ST
-module B = LowStar.Monotonic.Buffer
 let bytes = Seq.seq UInt8.t
 let lbytes l = b:bytes{Seq.length b = l}
 

diff --git a/examples/data_structures/LowStar.Lens.Buffer.fst b/examples/data_structures/LowStar.Lens.Buffer.fst
@@ -18,7 +18,6 @@ open LowStar.Lens
 open FStar.HyperStack.ST
 module B = LowStar.Buffer
 module HS = FStar.HyperStack
-module HST = FStar.HyperStack.ST
 open FStar.Integers
 
 let mk #a #p #q (b:B.mbuffer a p q) (f:flavor b) (snap:HS.mem{B.live snap b})

diff --git a/examples/data_structures/LowStar.Lens.Tuple2.fst b/examples/data_structures/LowStar.Lens.Tuple2.fst
@@ -17,7 +17,6 @@ module LowStar.Lens.Tuple2
 open LowStar.Lens
 open FStar.HyperStack.ST
 module B = LowStar.Buffer
-module HS = FStar.HyperStack
 module HST = FStar.HyperStack.ST
 module LB = LowStar.Lens.Buffer
 

diff --git a/examples/data_structures/LowStar.Lens.fst b/examples/data_structures/LowStar.Lens.fst
@@ -17,7 +17,6 @@ module LowStar.Lens
 open FStar.HyperStack.ST
 module B = LowStar.Buffer
 module HS = FStar.HyperStack
-module HST = FStar.HyperStack.ST
 
 let mods (l:hs_lens 'a 'b) (h:HS.mem) =
   B.modifies (as_loc l.footprint) l.snapshot h /\

diff --git a/examples/data_structures/LowStar.Lens.fsti b/examples/data_structures/LowStar.Lens.fsti
@@ -17,7 +17,6 @@ module LowStar.Lens
 open FStar.HyperStack.ST
 module B = LowStar.Buffer
 module HS = FStar.HyperStack
-module HST = FStar.HyperStack.ST
 
 (* This module provides a more abstract way of verifying Low*
    programs.

diff --git a/examples/dm4free/FStar.DM4F.Heap.fsti b/examples/dm4free/FStar.DM4F.Heap.fsti
@@ -18,7 +18,6 @@ module FStar.DM4F.Heap
 open FStar.Classical
 open FStar.Set
 
-module F = FStar.FunctionalExtensionality
 
 (* Heap is a tuple of a source of freshness (the no. of the next
    reference to be allocated) and a mapping of allocated raw

diff --git a/examples/doublylinkedlist/DoublyLinkedListIface.fst b/examples/doublylinkedlist/DoublyLinkedListIface.fst
@@ -26,7 +26,6 @@ module DLL = DoublyLinkedList
 
 module HS = FStar.HyperStack
 module HST = FStar.HyperStack.ST
-module G = FStar.Ghost
 module L = FStar.List.Pure
 module B = LowStar.Buffer
 

diff --git a/examples/doublylinkedlist/Example.fst b/examples/doublylinkedlist/Example.fst
@@ -16,10 +16,8 @@
 
 module Example
 
-module HS = FStar.HyperStack
 module HST = FStar.HyperStack.ST
 module B = LowStar.Buffer
-module DLL = DoublyLinkedListIface
 module L = FStar.List.Tot
 
 open DoublyLinkedListIface

diff --git a/examples/dsls/stlc/STLC.Infer.fst b/examples/dsls/stlc/STLC.Infer.fst
@@ -17,7 +17,6 @@
 module STLC.Infer
 module T = FStar.Tactics.V2
 module R = FStar.Reflection.V2
-module L = FStar.List.Tot
 module RT = FStar.Reflection.Typing
 open STLC.Core
 

diff --git a/examples/generic/Interop.fst b/examples/generic/Interop.fst
@@ -11,7 +11,6 @@ module Interop
 open FStar.FunctionalExtensionality
 open FStar.Integers
 open FStar.HyperStack.ST
-module M = FStar.Map
 module HS = FStar.HyperStack
 
 (* A primitive to update the state monolithically with the result of a ghost function *)

diff --git a/examples/interactive/FStar.InteractiveHelpers.ParseTest.fst b/examples/interactive/FStar.InteractiveHelpers.ParseTest.fst
@@ -1,8 +1,5 @@
 module FStar.InteractiveHelpers.ParseTest
 
-module HS = FStar.HyperStack
-module ST = FStar.HyperStack.ST
-module B = LowStar.Buffer
 
 open FStar.List
 open FStar.Tactics.V2

diff --git a/examples/interactive/FStar.InteractiveHelpers.Tutorial.fst b/examples/interactive/FStar.InteractiveHelpers.Tutorial.fst
@@ -16,7 +16,6 @@ open FStar.InteractiveHelpers.Tutorial.Definitions
 /// will need to restart the F* mode), which means that if you intend to use the
 /// extended mode while working on a file, you have to make sure F* will load
 /// FStar.InteractiveHelpers:
-module FI = FStar.InteractiveHelpers
 /// alternatively if you're not afraid of shadowing:
 /// open FStar.InteractiveHelpers
 

diff --git a/examples/kv_parsing/EnumParsing.fst b/examples/kv_parsing/EnumParsing.fst
@@ -31,7 +31,6 @@ open FStar.HyperStack
 open FStar.HyperStack.ST
 
 module U8 = FStar.UInt8
-module U16 = FStar.UInt16
 module U32 = FStar.UInt32
 
 (*! Pure model *)

diff --git a/examples/kv_parsing/Parsing.fst b/examples/kv_parsing/Parsing.fst
@@ -31,9 +31,7 @@ module C = C
 open C.Loops
 
 module U8 = FStar.UInt8
-module U16 = FStar.UInt16
 module U32 = FStar.UInt32
-module Cast = FStar.Int.Cast
 
 type byte = U8.t
 let bytes = seq byte

diff --git a/examples/kv_parsing/PureEncoder.fst b/examples/kv_parsing/PureEncoder.fst
@@ -16,9 +16,7 @@
 module PureEncoder
 
 open FStar.Seq
-module U16 = FStar.UInt16
 module U32 = FStar.UInt32
-module Cast = FStar.Int.Cast
 module List = FStar.List.Tot
 
 open KeyValue

diff --git a/examples/kv_parsing/PureParser.fst b/examples/kv_parsing/PureParser.fst
@@ -21,10 +21,7 @@ open IntegerParsing
 
 open FStar.Seq
 open FStar.Krml.Endianness
-module U8 = FStar.UInt8
-module U16 = FStar.UInt16
 module U32 = FStar.UInt32
-module Cast = FStar.Int.Cast
 
 (*** Spec-level pure parsing to values *)
 

diff --git a/examples/kv_parsing/Serializer.fst b/examples/kv_parsing/Serializer.fst
@@ -20,9 +20,7 @@ open FStar.HyperStack
 open FStar.HyperStack.ST
 open FStar.Ghost
 module B = FStar.Buffer
-module U16 = FStar.UInt16
 module U32 = FStar.UInt32
-module Cast = FStar.Int.Cast
 
 open KeyValue
 open Slice

diff --git a/examples/kv_parsing/Serializing.fst b/examples/kv_parsing/Serializing.fst
@@ -29,10 +29,7 @@ open FStar.Ghost
 module C = C
 open C.Loops
 
-module U8 = FStar.UInt8
-module U16 = FStar.UInt16
 module U32 = FStar.UInt32
-module Cast = FStar.Int.Cast
 
 (* Note the lack of definitions around encoding, the pure specification for serialization.
 

diff --git a/examples/kv_parsing/ValidatedAccess.fst b/examples/kv_parsing/ValidatedAccess.fst
@@ -31,9 +31,7 @@ open C.Loops
 
 module B = FStar.Buffer
 
-module U16 = FStar.UInt16
 module U32 = FStar.UInt32
-module I32 = FStar.Int32
 module Cast = FStar.Int.Cast
 
 (*** API to access validated but unparsed key-value buffer *)

diff --git a/examples/kv_parsing/ValidatedParser.fst b/examples/kv_parsing/ValidatedParser.fst
@@ -29,9 +29,7 @@ open FStar.HyperStack.ST
 
 module B = FStar.Buffer
 
-module U16 = FStar.UInt16
 module U32 = FStar.UInt32
-module Cast = FStar.Int.Cast
 
 (*** API using validated but unparsed key-value buffer *)
 

diff --git a/examples/kv_parsing/Validator.fst b/examples/kv_parsing/Validator.fst
@@ -29,11 +29,8 @@ module C = C
 // special karamel support for looping
 open C.Loops
 
-module B = FStar.Buffer
 
-module U16 = FStar.UInt16
 module U32 = FStar.UInt32
-module Cast = FStar.Int.Cast
 
 (*** Stateful validation of input buffer *)
 

diff --git a/examples/kv_parsing/VectorParsing.fst b/examples/kv_parsing/VectorParsing.fst
@@ -32,7 +32,6 @@ open C.Loops
 
 module B = FStar.Buffer
 
-module U8 = FStar.UInt8
 module U16 = FStar.UInt16
 module U32 = FStar.UInt32
 module Cast = FStar.Int.Cast

diff --git a/examples/layeredeffects/AlgForAll.fst b/examples/layeredeffects/AlgForAll.fst
@@ -1,9 +1,6 @@
 module AlgForAll
 
 open FStar.Calc
-module FE = FStar.FunctionalExtensionality
-module F = FStar.FunctionalExtensionality
-module W = FStar.WellFounded
 module T = FStar.Tactics.V2
 module ID5 = ID5
 open Alg

diff --git a/examples/layeredeffects/AlgHeap.fst b/examples/layeredeffects/AlgHeap.fst
@@ -5,10 +5,7 @@ module AlgHeap
 open FStar.Tactics.V2
 open FStar.List.Tot
 open FStar.Universe
-module L = Lattice
-module Ghost = FStar.Ghost
 module Map = FStar.Map
-module T = FStar.Tactics.V2
 
 type loc = int
 type state = Map.t loc int

diff --git a/examples/layeredeffects/AlgWP.fst b/examples/layeredeffects/AlgWP.fst
@@ -7,9 +7,6 @@ WP from intensional information about the operations in the tree. *)
 
 open FStar.List.Tot
 open FStar.Calc
-module FE = FStar.FunctionalExtensionality
-module F = FStar.FunctionalExtensionality
-module W = FStar.WellFounded
 module T = FStar.Tactics.V2
 // #show-options
 module ID5 = ID5

diff --git a/examples/layeredeffects/GenericPartialDM4A.fst b/examples/layeredeffects/GenericPartialDM4A.fst
@@ -3,9 +3,6 @@ module GenericPartialDM4A
 open FStar.Tactics.V2
 open FStar.Calc
 open FStar.FunctionalExtensionality
-module F = FStar.FunctionalExtensionality
-module W = FStar.WellFounded
-module T = FStar.Tactics.V2
 open FStar.Preorder
 
 // m is a monad.

diff --git a/examples/layeredeffects/GenericTotalDM4A.fst b/examples/layeredeffects/GenericTotalDM4A.fst
@@ -3,9 +3,6 @@ module GenericTotalDM4A
 open FStar.Tactics.V2
 open FStar.Calc
 open FStar.FunctionalExtensionality
-module F = FStar.FunctionalExtensionality
-module W = FStar.WellFounded
-module T = FStar.Tactics.V2
 open FStar.Preorder
 
 // m is a monad.

diff --git a/examples/layeredeffects/HoareST.fst b/examples/layeredeffects/HoareST.fst
@@ -20,7 +20,6 @@ open FStar.Heap
 open FStar.ST
 
 module P = FStar.Preorder
-module ST = FStar.ST
 
 /// ST effect implemented as a layered effect over STATE
 

diff --git a/examples/layeredeffects/HoareSTPolyBind.fst b/examples/layeredeffects/HoareSTPolyBind.fst
@@ -20,7 +20,6 @@ open FStar.Heap
 open FStar.ST
 
 module P = FStar.Preorder
-module ST = FStar.ST
 
 
 /// ST effect implemented as a layered effect over STATE

diff --git a/examples/layeredeffects/ID3.fst b/examples/layeredeffects/ID3.fst
@@ -71,7 +71,6 @@ sub_effect PURE ~> ID = lift_pure_nd
 val test_f : unit -> ID int (as_pure_wp (fun p -> p 5 /\ p 3))
 let test_f () = 3
 
-module T = FStar.Tactics.V2
 
 let l () : int =
   reify (test_f ())

diff --git a/examples/layeredeffects/ND.fst b/examples/layeredeffects/ND.fst
@@ -7,9 +7,6 @@ open FStar.List.Tot
 open FStar.Calc
 
 open FStar.FunctionalExtensionality
-module F = FStar.FunctionalExtensionality
-module W = FStar.WellFounded
-module T = FStar.Tactics.V2
 
 // m is a monad. In this particular example, lists
 val m (a : Type u#a) : Type u#a

diff --git a/examples/layeredeffects/Z3EncodingIssue.fst b/examples/layeredeffects/Z3EncodingIssue.fst
@@ -38,7 +38,6 @@ open FStar.Integers
 
 open FStar.HyperStack.ST
 
-module HS = FStar.HyperStack
 
 module B = LowStar.Buffer
Original file line number	Diff line number	Diff line change
Expand Up		@@ -38,7 +38,6 @@ open FStar.Integers

		open FStar.HyperStack.ST

		module HS = FStar.HyperStack

		module B = LowStar.Buffer

Expand Down