Run $FSTAR/.scripts/remove_all_unused_opens.sh .

FStarLang · Feb 18, 2025 · dac35ec · dac35ec
1 parent 55fac43
commit dac35ec
Show file tree

Hide file tree

Showing 159 changed files with 2 additions and 268 deletions.
diff --git a/lib/common/Pulse.Lib.Core.fsti b/lib/common/Pulse.Lib.Core.fsti
@@ -19,8 +19,6 @@ open FStar.Ghost
 open PulseCore.FractionalPermission
 open PulseCore.Observability
 open FStar.PCM
-module G = FStar.Ghost
-module Set = FStar.Set
 module T = FStar.Tactics.V2
 open Pulse.Lib.Dv {}
 open FStar.ExtractAs

diff --git a/lib/core/Pulse.Lib.Core.fst b/lib/core/Pulse.Lib.Core.fst
@@ -17,7 +17,6 @@ module Pulse.Lib.Core
 module I = PulseCore.InstantiatedSemantics
 module A = PulseCore.Atomic
 module T = FStar.Tactics.V2
-module F = FStar.FunctionalExtensionality
 open PulseCore.InstantiatedSemantics
 open PulseCore.FractionalPermission
 open PulseCore.Observability

diff --git a/lib/core/PulseCore.Action.fst b/lib/core/PulseCore.Action.fst
@@ -367,7 +367,6 @@ let exists_equiv (#a:_) (#p:a -> slprop)
     let pf = FStar.Squash.return_squash pf in
     I.slprop_equiv_elim (op_exists_Star p) (exists* x. p x)
 
-module T = FStar.Tactics
 let fresh_invariant ctx p = fun #ictx -> ITA.fresh_invariant ictx p ctx
 
 let inames_live_inv (i:iref) (p:slprop) = fun #ictx -> ITA.inames_live_inv ictx i p

diff --git a/lib/core/PulseCore.Action.fsti b/lib/core/PulseCore.Action.fsti
@@ -16,9 +16,7 @@
 
 module PulseCore.Action
 
-module S = FStar.Set
 module I = PulseCore.InstantiatedSemantics
-module PP = PulseCore.Preorder
 module Sep = PulseCore.IndirectionTheorySep
 open FStar.PCM
 open FStar.Ghost

diff --git a/lib/core/PulseCore.Atomic.fsti b/lib/core/PulseCore.Atomic.fsti
@@ -334,7 +334,6 @@ val buy1 ()
 // References
 ////////////////////////////////////////////////////////////////////////
 open FStar.PCM
-module PP = PulseCore.Preorder
 
 val pts_to_not_null
     (#a:Type u#1)

diff --git a/lib/core/PulseCore.CompactHeapSig.fst b/lib/core/PulseCore.CompactHeapSig.fst
@@ -2,8 +2,6 @@ module PulseCore.CompactHeapSig
 open FStar.Ghost
 open FStar.PCM
 open PulseCore.HeapSig
-module H2 = PulseCore.Heap2
-module ST = PulseCore.HoareStateMonad
 module CM = FStar.Algebra.CommMonoid
 open FStar.Tactics.Typeclasses
 

diff --git a/lib/core/PulseCore.Heap.fst b/lib/core/PulseCore.Heap.fst
@@ -17,7 +17,6 @@ module PulseCore.Heap
 module F = FStar.FunctionalExtensionality
 open FStar.FunctionalExtensionality
 open FStar.PCM
-module Frac = PulseCore.FractionalPermission
 module PP = PulseCore.Preorder
 
 #set-options "--fuel 1 --ifuel 1"
@@ -270,7 +269,6 @@ let join_empty_inverse (m0 m1:heap)
 ////////////////////////////////////////////////////////////////////////////////
 let slprop = p:(heap ^-> prop) { heap_prop_is_affine p }
 
-module W = FStar.WellFounded
 
 
 let interp (p:slprop u#a) (m:heap u#a)

diff --git a/lib/core/PulseCore.Heap.fsti b/lib/core/PulseCore.Heap.fsti
@@ -16,7 +16,6 @@
 module PulseCore.Heap
 open FStar.Ghost
 open FStar.PCM
-module Frac = PulseCore.FractionalPermission
 
 /// This module defines the behavior of a structured heap where each memory cell is governed by
 /// a partial commutative monoid. This PCM structure is reused for the entire heap as it is possible

diff --git a/lib/core/PulseCore.Heap2.fst b/lib/core/PulseCore.Heap2.fst
@@ -3,8 +3,6 @@ module F = FStar.FunctionalExtensionality
 open FStar.FunctionalExtensionality
 open FStar.PCM
 open PulseCore.Tags
-module Frac = PulseCore.FractionalPermission
-module PP = PulseCore.Preorder
 module H = PulseCore.Heap
 
 noeq

diff --git a/lib/core/PulseCore.HeapSig.fst b/lib/core/PulseCore.HeapSig.fst
@@ -1,8 +1,6 @@
 module PulseCore.HeapSig
 open FStar.Ghost
 open FStar.PCM
-module H2 = PulseCore.Heap2
-module ST = PulseCore.HoareStateMonad
 module CM = FStar.Algebra.CommMonoid
 
 let star_commutative #h p q =

diff --git a/lib/core/PulseCore.IndirectionTheoryActions.fst b/lib/core/PulseCore.IndirectionTheoryActions.fst
@@ -14,10 +14,7 @@
    limitations under the License.
 *)
 module PulseCore.IndirectionTheoryActions
-module F = FStar.FunctionalExtensionality
-module T = FStar.Tactics
 module PM = PulseCore.MemoryAlt
-module HST = PulseCore.HoareStateMonad
 open FStar.Ghost
 
 let pm_sep_laws () : squash (

diff --git a/lib/core/PulseCore.IndirectionTheoryActions.fsti b/lib/core/PulseCore.IndirectionTheoryActions.fsti
@@ -1,6 +1,4 @@
 module PulseCore.IndirectionTheoryActions
-module F = FStar.FunctionalExtensionality
-module T = FStar.Tactics
 module PM = PulseCore.MemoryAlt
 module HST = PulseCore.HoareStateMonad
 open PulseCore.IndirectionTheorySep

diff --git a/lib/core/PulseCore.IndirectionTheorySep.fst b/lib/core/PulseCore.IndirectionTheorySep.fst
@@ -19,8 +19,6 @@ open PulseCore.KnotInstantiation
 open FStar.FunctionalExtensionality
 module F = FStar.FunctionalExtensionality
 module PM = PulseCore.MemoryAlt
-module HS = PulseCore.HeapSig
-module IT = PulseCore.IndirectionTheory
 open FStar.Ghost {erased, hide, reveal}
 
 let timeless_heap_le (a b: timeless_heap_sig.mem) : prop =

diff --git a/lib/core/PulseCore.InstantiatedSemantics.fst b/lib/core/PulseCore.InstantiatedSemantics.fst
@@ -17,8 +17,6 @@ module PulseCore.InstantiatedSemantics
 
 module Sem = PulseCore.Semantics
 module Sep = PulseCore.IndirectionTheorySep
-module ITA = PulseCore.IndirectionTheoryActions
-module U = FStar.Universe
 module F = FStar.FunctionalExtensionality
 
 open PulseCore.IndirectionTheorySep
@@ -80,7 +78,6 @@ let slprop_equiv_elim p q = ()
 let slprop_equiv_unit p = unsquash ()
 let slprop_equiv_comm p1 p2 = unsquash ()
 let slprop_equiv_assoc p1 p2 p3 = unsquash ()
-module T = FStar.Tactics.V2
 let slprop_equiv_exists 
     (#a:Type)
     (p q: a -> slprop)

diff --git a/lib/core/PulseCore.KnotInstantiation.fst b/lib/core/PulseCore.KnotInstantiation.fst
@@ -18,8 +18,6 @@ module PulseCore.KnotInstantiation
 open PulseCore.IndirectionTheory
 open FStar.FunctionalExtensionality
 module F = FStar.FunctionalExtensionality
-module PM = PulseCore.MemoryAlt
-module HS = PulseCore.HeapSig
 module IT = PulseCore.IndirectionTheory
 open FStar.Ghost {erased, hide, reveal}
 

diff --git a/lib/core/PulseCore.MemoryAlt.fst b/lib/core/PulseCore.MemoryAlt.fst
@@ -17,9 +17,7 @@
 module PulseCore.MemoryAlt
 open FStar.Ghost
 open FStar.PCM
-module PST = PulseCore.HoareStateMonad
 module U = FStar.Universe
-module S = FStar.Set
 module CM = FStar.Algebra.CommMonoid
 module H = PulseCore.HeapSig
 module E = PulseCore.HeapExtension
@@ -169,7 +167,6 @@ let star  (p1 p2:slprop u#a)
 : slprop u#a
 = sig.star p1 p2
 
-module F = FStar.FunctionalExtensionality
 let h_exists (#a:Type u#b) (f: (a -> slprop u#a))
 : slprop u#a
 = H.exists_ #sig #a (fun x -> reveal_slprop (f x))

diff --git a/lib/core/PulseCore.MemoryAlt.fsti b/lib/core/PulseCore.MemoryAlt.fsti
@@ -19,7 +19,6 @@ open FStar.Ghost
 open FStar.PCM
 module PST = PulseCore.HoareStateMonad
 module U = FStar.Universe
-module S = FStar.Set
 module CM = FStar.Algebra.CommMonoid
 /// This module adds memory invariants to the heap to expose the
 /// final interface for Pulse's PCM-based memory model.

diff --git a/lib/pulse/lib/Pulse.Lib.AnchoredReference.fst b/lib/pulse/lib/Pulse.Lib.AnchoredReference.fst
@@ -24,7 +24,6 @@ open PulseCore.Preorder
 open Pulse.Lib.FractionalAnchoredPreorder
 module FRAP = Pulse.Lib.FractionalAnchoredPreorder
 module GPR = Pulse.Lib.GhostPCMReference
-module U32 = FStar.UInt32
 module T = FStar.Tactics
 
 let carrier (#a:Type0) (#p:preorder a) (#anc:anchor_rel p)

diff --git a/lib/pulse/lib/Pulse.Lib.AnchoredReference.fsti b/lib/pulse/lib/Pulse.Lib.AnchoredReference.fsti
@@ -22,7 +22,6 @@ open FStar.Preorder
 open Pulse.Lib.FractionalAnchoredPreorder
 #lang-pulse
 
-module U32 = FStar.UInt32
 module T = FStar.Tactics
 
 [@@erasable]

diff --git a/lib/pulse/lib/Pulse.Lib.Array.fst b/lib/pulse/lib/Pulse.Lib.Array.fst
@@ -16,7 +16,6 @@
 
 module Pulse.Lib.Array
 #lang-pulse
-module PM = Pulse.Main
 open Pulse.Lib.Core
 open Pulse.Lib.Reference
 open Pulse.Lib.Array.Core
@@ -26,7 +25,6 @@ module US = FStar.SizeT
 module U8 = FStar.UInt8
 open Pulse.Lib.BoundedIntegers
 module A = Pulse.Lib.Array.Core
-module R = Pulse.Lib.Reference
 
 #set-options "--print_implicits"
 

diff --git a/lib/pulse/lib/Pulse.Lib.BigReference.fsti b/lib/pulse/lib/Pulse.Lib.BigReference.fsti
@@ -18,7 +18,6 @@ module Pulse.Lib.BigReference
 open Pulse.Lib.Core
 open PulseCore.FractionalPermission
 open FStar.Ghost
-module U32 = FStar.UInt32
 module T = FStar.Tactics
 val ref ([@@@unused]a:Type u#2) : Type u#0
 

diff --git a/lib/pulse/lib/Pulse.Lib.Box.fsti b/lib/pulse/lib/Pulse.Lib.Box.fsti
@@ -22,7 +22,6 @@ open PulseCore.FractionalPermission
 open Pulse.Lib.Core
 open Pulse.Class.PtsTo
 
-module U32 = FStar.UInt32
 module T = FStar.Tactics.V2
 
 module R = Pulse.Lib.Reference

diff --git a/lib/pulse/lib/Pulse.Lib.Deque.fst b/lib/pulse/lib/Pulse.Lib.Deque.fst
@@ -5,9 +5,6 @@ open Pulse.Lib.Pervasives
 open Pulse.Lib.Stick.Util
 open FStar.List.Tot
 open Pulse.Lib.Trade
-module T = FStar.Tactics
-module I = Pulse.Lib.Stick.Util
-module FA = Pulse.Lib.Forall.Util
 module Box = Pulse.Lib.Box
 
 noeq

diff --git a/lib/pulse/lib/Pulse.Lib.DequeRef.fst b/lib/pulse/lib/Pulse.Lib.DequeRef.fst
@@ -3,7 +3,6 @@ module Pulse.Lib.DequeRef
 open Pulse.Lib.Pervasives
 open Pulse.Lib.Deque
 module B = Pulse.Lib.Box
-module DQ = Pulse.Lib.Deque
 open FStar.List.Tot
 
 let dq (t:Type0) = B.box (deque t)

diff --git a/lib/pulse/lib/Pulse.Lib.HashTable.Type.fsti b/lib/pulse/lib/Pulse.Lib.HashTable.Type.fsti
@@ -18,7 +18,6 @@ module Pulse.Lib.HashTable.Type
 
 open Pulse.Lib.Pervasives
 module V = Pulse.Lib.Vec
-module R = Pulse.Lib.Reference
 module SZ = FStar.SizeT
 
 open Pulse.Lib.HashTable.Spec

diff --git a/lib/pulse/lib/Pulse.Lib.HashTable.fsti b/lib/pulse/lib/Pulse.Lib.HashTable.fsti
@@ -21,7 +21,6 @@ open Pulse.Lib.HashTable.Spec
 open Pulse.Lib.HashTable.Type
 
 module V = Pulse.Lib.Vec
-module R = Pulse.Lib.Reference
 module SZ = FStar.SizeT
 module PHT = Pulse.Lib.HashTable.Spec
 

diff --git a/lib/pulse/lib/Pulse.Lib.HigherReference.fsti b/lib/pulse/lib/Pulse.Lib.HigherReference.fsti
@@ -19,7 +19,6 @@ open Pulse.Lib.Core
 open PulseCore.FractionalPermission
 open FStar.Ghost
 open Pulse.Class.PtsTo
-module U32 = FStar.UInt32
 module T = FStar.Tactics
 val ref ([@@@unused]a:Type u#1) : Type u#0
 

diff --git a/lib/pulse/lib/Pulse.Lib.LinkedList.fst b/lib/pulse/lib/Pulse.Lib.LinkedList.fst
@@ -19,7 +19,6 @@ module Pulse.Lib.LinkedList
 open Pulse.Lib.Pervasives
 open Pulse.Lib.Stick.Util
 open FStar.List.Tot
-module T = FStar.Tactics
 module I = Pulse.Lib.Stick.Util
 module FA = Pulse.Lib.Forall.Util
 

diff --git a/lib/pulse/lib/Pulse.Lib.MonotonicGhostRef.fst b/lib/pulse/lib/Pulse.Lib.MonotonicGhostRef.fst
@@ -5,7 +5,6 @@ open Pulse.Lib.GhostPCMReference
 open FStar.Preorder
 module GR = Pulse.Lib.GhostPCMReference
 module FP = Pulse.Lib.PCM.FractionalPreorder
-module PP = PulseCore.Preorder
 
 
 let mref (#t:Type) (p:preorder t) = GR.gref (FP.fp_pcm p)

diff --git a/lib/pulse/lib/Pulse.Lib.MonotonicGhostRef.fsti b/lib/pulse/lib/Pulse.Lib.MonotonicGhostRef.fsti
@@ -3,9 +3,6 @@ module Pulse.Lib.MonotonicGhostRef
 open Pulse.Lib.Pervasives
 open Pulse.Lib.GhostPCMReference
 open FStar.Preorder
-module GR = Pulse.Lib.GhostPCMReference
-module FP = Pulse.Lib.PCM.FractionalPreorder
-module PP = PulseCore.Preorder
 
 let as_prop (t:Type0) = t <==> True
 

diff --git a/lib/pulse/lib/Pulse.Lib.PCM.FractionalPreorder.fst b/lib/pulse/lib/Pulse.Lib.PCM.FractionalPreorder.fst
@@ -21,7 +21,6 @@ open FStar.Preorder
 open PulseCore.Preorder
 open PulseCore.FractionalPermission
 
-module L = FStar.List.Tot
 
 type pcm_carrier (#a:Type u#a) (p:preorder a) : Type u#a = option perm & hist p
 

diff --git a/lib/pulse/lib/Pulse.Lib.Primitives.fst b/lib/pulse/lib/Pulse.Lib.Primitives.fst
@@ -17,7 +17,6 @@
 module Pulse.Lib.Primitives
 #lang-pulse
 
-module B = Pulse.Lib.Box
 
 friend Pulse.Lib.Box
 

diff --git a/lib/pulse/lib/Pulse.Lib.SeqMatch.fst b/lib/pulse/lib/Pulse.Lib.SeqMatch.fst
@@ -20,7 +20,6 @@ open Pulse.Lib.OnRange
 open Pulse.Lib.Stick.Util
 
 module Seq = FStar.Seq
-module SZ = FStar.SizeT
 
 (* `seq_list_match` describes how to match a sequence of low-level
 values (the low-level contents of an array) with a list of high-level

diff --git a/lib/pulse/lib/Pulse.Lib.SeqMatch.fsti b/lib/pulse/lib/Pulse.Lib.SeqMatch.fsti
@@ -20,7 +20,6 @@ include Pulse.Lib.Pervasives
 open Pulse.Lib.Stick
 
 module Seq = FStar.Seq
-module SZ = FStar.SizeT
 
 (* `seq_list_match` describes how to match a sequence of low-level
 values (the low-level contents of an array) with a list of high-level

diff --git a/lib/pulse/lib/Pulse.Lib.Swap.Array.fst b/lib/pulse/lib/Pulse.Lib.Swap.Array.fst
@@ -16,7 +16,6 @@
 
 module Pulse.Lib.Swap.Array
 #lang-pulse
-module R = Pulse.Lib.Reference
 module Prf = Pulse.Lib.Swap.Spec
 open Pulse.Lib.Swap.Common
 #set-options "--fuel 2 --ifuel 1"

diff --git a/lib/pulse/lib/Pulse.Lib.Swap.Slice.fst b/lib/pulse/lib/Pulse.Lib.Swap.Slice.fst
@@ -16,7 +16,6 @@
 
 module Pulse.Lib.Swap.Slice
 #lang-pulse
-module R = Pulse.Lib.Reference
 module Prf = Pulse.Lib.Swap.Spec
 open Pulse.Lib.Swap.Common
 #set-options "--fuel 2 --ifuel 1"

diff --git a/lib/pulse/lib/Pulse.Lib.Task.fst b/lib/pulse/lib/Pulse.Lib.Task.fst
@@ -30,8 +30,6 @@ open Pulse.Lib.SpinLock
 module RTC   = FStar.ReflexiveTransitiveClosure
 module FRAP  = Pulse.Lib.FractionalAnchoredPreorder
 module AR    = Pulse.Lib.AnchoredReference
-module Big   = Pulse.Lib.BigReference
-module Ghost = Pulse.Lib.GhostReference
 
 noeq
 type task_state : Type0 =

diff --git a/lib/pulse/lib/pledge/Pulse.Lib.Shift.fst b/lib/pulse/lib/pledge/Pulse.Lib.Shift.fst
@@ -20,7 +20,6 @@ open FStar.Ghost
 open Pulse.Class.Duplicable
 open Pulse.Lib.Pervasives
 
-module T = FStar.Tactics
 
 let shift_elim_t is hyp extra concl : Type u#4 =
   unit -> stt_ghost unit is (extra ** hyp) (fun _ -> concl)

diff --git a/lib/pulse/lib/pledge/Pulse.Lib.SmallTrade.fst b/lib/pulse/lib/pledge/Pulse.Lib.SmallTrade.fst
@@ -21,7 +21,6 @@ open FStar.Ghost
 open Pulse.Lib.Core
 open Pulse.Lib.Pervasives
 
-module T = FStar.Tactics
 
 type small_slprop = v:slprop { timeless v }
 

diff --git a/lib/pulse/lib/pledge/Pulse.Lib.Trade.fst b/lib/pulse/lib/pledge/Pulse.Lib.Trade.fst
@@ -19,7 +19,6 @@ module Pulse.Lib.Trade
 
 open Pulse.Lib.Pervasives
 
-module T = FStar.Tactics
 
 let trade_elim_t is hyp extra concl : Type u#4 =
   unit -> stt_ghost unit is (extra ** hyp) (fun _ -> concl)

diff --git a/pulse2rust/src/Pulse2Rust.Deps.fst b/pulse2rust/src/Pulse2Rust.Deps.fst
@@ -30,9 +30,7 @@ open RustBindings
 open FStarC.Class.Setlike
 
 module S = FStarC.Extraction.ML.Syntax
-module EUtil = FStarC.Extraction.ML.Util
 
-module UEnv = FStarC.Extraction.ML.UEnv
 
 let empty_defs : reachable_defs = RBSet.empty ()
 let singleton (p:S.mlpath) : reachable_defs = singleton (S.string_of_mlpath p)

diff --git a/pulse2rust/src/Pulse2Rust.Deps.fsti b/pulse2rust/src/Pulse2Rust.Deps.fsti
@@ -27,9 +27,7 @@ open Pulse2Rust.Extract
 open RustBindings
 
 module S = FStarC.Extraction.ML.Syntax
-module EUtil = FStarC.Extraction.ML.Util
 
-module UEnv = FStarC.Extraction.ML.UEnv
 
 val empty_defs : reachable_defs
 

diff --git a/pulse2rust/src/Pulse2Rust.Env.fst b/pulse2rust/src/Pulse2Rust.Env.fst
@@ -26,9 +26,7 @@ open Pulse2Rust.Rust.Syntax
 
 open RustBindings
 
-module S = FStarC.Extraction.ML.Syntax
 
-module UEnv = FStarC.Extraction.ML.UEnv
 
 let fail (s:string) =
   failwith (format1 "Pulse to Rust extraction failed: %s" s)