From 9b7eb79ab54644f0a8bd8d982b75f5318d214cdf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Fri, 14 Feb 2025 14:08:21 -0800 Subject: [PATCH] Run `.scripts/remove_all_unused_opens.sh src/ ulib/ doc/ tests/ examples/ contrib/` --- contrib/CoreCrypto/ml/Tests.ml | 3 --- doc/book/code/ContextPollution.fst | 3 --- doc/book/code/exercises/Part3.Typeclasses.fst | 1 - doc/old/tutorial/code/exercises/LowStar.Ex3.fst | 3 --- doc/old/tutorial/code/solutions/Ex12a1.Cap.fst | 1 - doc/old/tutorial/code/solutions/LowStar.Ex3.fst | 2 -- examples/crypto/HyE.AE.fst | 1 - examples/crypto/HyE.AE.fsti | 1 - examples/crypto/HyE.HCCA2.fst | 2 -- examples/crypto/HyE.HCCA2.fsti | 1 - examples/crypto/HyE.RSA.fst | 1 - examples/crypto/OPLSS.Log.fst | 1 - examples/crypto/OPLSS.fst | 3 --- examples/data_structures/LowStar.Lens.Buffer.fst | 1 - examples/data_structures/LowStar.Lens.Tuple2.fst | 1 - examples/data_structures/LowStar.Lens.fst | 1 - examples/data_structures/LowStar.Lens.fsti | 1 - examples/dm4free/FStar.DM4F.Heap.fsti | 1 - examples/doublylinkedlist/DoublyLinkedListIface.fst | 1 - examples/doublylinkedlist/Example.fst | 2 -- examples/dsls/stlc/STLC.Infer.fst | 1 - examples/generic/Interop.fst | 1 - .../interactive/FStar.InteractiveHelpers.ParseTest.fst | 3 --- .../interactive/FStar.InteractiveHelpers.Tutorial.fst | 1 - examples/kv_parsing/EnumParsing.fst | 1 - examples/kv_parsing/Parsing.fst | 2 -- examples/kv_parsing/PureEncoder.fst | 2 -- examples/kv_parsing/PureParser.fst | 3 --- examples/kv_parsing/Serializer.fst | 2 -- examples/kv_parsing/Serializing.fst | 3 --- examples/kv_parsing/ValidatedAccess.fst | 2 -- examples/kv_parsing/ValidatedParser.fst | 2 -- examples/kv_parsing/Validator.fst | 3 --- examples/kv_parsing/VectorParsing.fst | 1 - examples/layeredeffects/AlgForAll.fst | 3 --- examples/layeredeffects/AlgHeap.fst | 3 --- examples/layeredeffects/AlgWP.fst | 3 --- examples/layeredeffects/GenericPartialDM4A.fst | 3 --- examples/layeredeffects/GenericTotalDM4A.fst | 3 --- examples/layeredeffects/HoareST.fst | 1 - examples/layeredeffects/HoareSTPolyBind.fst | 1 - examples/layeredeffects/ID3.fst | 1 - examples/layeredeffects/ND.fst | 3 --- examples/layeredeffects/Z3EncodingIssue.fst | 1 - .../everparse/LowParseWriters.LowParse.fst | 1 - .../everparse/tls/Negotiation.Writers.Aux.fsti | 1 - .../everparse/tls/Negotiation.Writers.Aux2.fsti | 1 - .../everparse/tls/Negotiation.Writers.NoHoare.Aux.fst | 1 - .../everparse/tls/Negotiation.Writers.NoHoare.Aux2.fst | 1 - examples/low-mitls-experiments/HSL.fsti | 1 - examples/low-mitls-experiments/ImmutableBuffer.fst | 1 - examples/miniparse/MiniParse.Impl.List.fst | 1 - examples/miniparse/MiniParse.Impl.TSum.fst | 1 - examples/miniparse/MiniParse.Spec.Base.fst | 1 - examples/miniparse/MiniParse.Spec.Combinators.fst | 2 -- examples/miniparse/MiniParse.Spec.List.fst | 2 -- examples/miniparse/MiniParse.Spec.List.fsti | 1 - examples/miniparse/MiniParse.Tac.Impl.fst | 1 - examples/miniparse/MiniParseExample2.fst | 1 - examples/native_tactics/Imp.List.fst | 1 - examples/old/Buffers.fst | 1 - examples/old/Setoids.Crypto.fst | 1 - examples/old/tls-record-layer/LowCProvider/Tests.ml | 1 - .../crypto/Crypto.AEAD.Chacha20Poly1305.fst | 1 - .../old/tls-record-layer/crypto/Crypto.AEAD.Decrypt.fst | 3 --- .../old/tls-record-layer/crypto/Crypto.AEAD.Encoding.fst | 2 -- .../tls-record-layer/crypto/Crypto.AEAD.Encrypt.Aux.fst | 1 - .../crypto/Crypto.AEAD.Encrypt.Ideal.Invariant.fst | 3 --- .../crypto/Crypto.AEAD.Encrypt.Invariant.fst | 2 -- .../old/tls-record-layer/crypto/Crypto.AEAD.Encrypt.fst | 2 -- .../crypto/Crypto.AEAD.Enxor.Invariant.fst | 3 --- .../tls-record-layer/crypto/Crypto.AEAD.EnxorDexor.fst | 1 - .../tls-record-layer/crypto/Crypto.AEAD.Invariant.fst | 1 - .../crypto/Crypto.AEAD.MAC_Wrapper.Invariant.fst | 1 - .../tls-record-layer/crypto/Crypto.AEAD.Wrappers.CMA.fst | 2 -- .../crypto/Crypto.AEAD.Wrappers.Encoding.fst | 2 -- .../tls-record-layer/crypto/Crypto.AEAD.Wrappers.PRF.fst | 1 - examples/old/tls-record-layer/crypto/Crypto.AEAD.fst | 9 --------- examples/old/tls-record-layer/crypto/Crypto.KrmlTest.fst | 7 ------- .../old/tls-record-layer/crypto/Crypto.Symmetric.AES.fst | 3 --- .../tls-record-layer/crypto/Crypto.Symmetric.AES128.fst | 3 --- .../tls-record-layer/crypto/Crypto.Symmetric.Bytes.fst | 1 - .../crypto/Crypto.Symmetric.Chacha20.fst | 2 -- .../tls-record-layer/crypto/Crypto.Symmetric.Cipher.fst | 2 -- .../Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part1.fst | 1 - .../Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part2.fst | 3 --- .../Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part3.fst | 3 --- .../Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part5.fst | 1 - .../Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part6.fst | 1 - .../crypto/Crypto.Symmetric.Poly1305.Bignum.fst | 1 - .../crypto/Crypto.Symmetric.Poly1305.Spec.fst | 2 -- .../crypto/Crypto.Symmetric.Poly1305.fst | 1 - examples/old/tls-record-layer/crypto/Crypto.WIP.fst | 7 ------- .../tls-record-layer/crypto/stale/Curve.AddAndDouble.fst | 2 -- .../old/tls-record-layer/crypto/stale/Curve.Bignum.fst | 2 -- .../tls-record-layer/crypto/stale/Curve.Fdifference.fst | 2 -- .../old/tls-record-layer/crypto/stale/Curve.Fproduct.fst | 2 -- .../old/tls-record-layer/crypto/stale/Curve.Fscalar.fst | 2 -- .../old/tls-record-layer/crypto/stale/Curve.Fsum.fst | 2 -- .../old/tls-record-layer/crypto/stale/Curve.FsumWide.fst | 3 --- .../old/tls-record-layer/crypto/stale/Curve.Modulo.fst | 1 - .../old/tls-record-layer/crypto/stale/Curve.Point.fst | 2 -- .../old/ulib/hyperstack/FStar.StackArray.fst | 1 - .../old/tls-record-layer/old/ulib/hyperstack/chacha.fst | 1 - examples/preorders/Closure.fst | 1 - examples/preorders/NatHeap.fsti | 1 - examples/regional/RVector.fst | 1 - examples/rel/IfcMonitorTest.fst | 1 - examples/tactics/Imp.fst | 1 - examples/tactics/Printers.fst | 1 - examples/tactics/old/StringPrinter.Rec.fst | 2 -- examples/typeclasses/Deriving.fst | 1 - src/basic/FStarC.Range.Type.fst | 1 - tests/bug-reports/closed/Bug1750.Aux.fst | 3 --- tests/bug-reports/closed/Bug2169.fst | 1 - tests/hacl/Lib.Exponentiation.Definition.fst | 1 - tests/hacl/Lib.Exponentiation.Definition.fsti | 1 - tests/machine_integers/Test02.fst | 1 - tests/machine_integers/TestChar.fst | 1 - tests/machine_integers/TestShift.fst | 6 ------ tests/micro-benchmarks/BinderAttributes.fst | 1 - tests/micro-benchmarks/BoxBitVec.fst | 1 - tests/micro-benchmarks/BvBinaryOps.fst | 2 -- .../NormPureSubtermsWithinComputations.fst | 1 - tests/micro-benchmarks/Test.Delta.Namespace.fst | 1 - tests/micro-benchmarks/TestWellFoundedRecursion.fst | 1 - tests/micro-benchmarks/TwoPhaseTC.fst | 1 - tests/struct/taggedunion.pos/Test.fst | 1 - tests/vale/X64.Vale.StateLemmas_i.fst | 1 - tests/vale/X64.Vale.StateLemmas_i.fsti | 1 - ulib/FStar.Bytes.fsti | 3 --- ulib/FStar.FiniteMap.Base.fsti | 1 - ulib/FStar.Matrix.fst | 1 - ulib/FStar.Modifies.fst | 2 -- ulib/FStar.ModifiesGen.fst | 1 - ulib/FStar.Monotonic.DependentMap.fst | 1 - ulib/FStar.Monotonic.HyperHeap.fst | 2 -- ulib/FStar.Printf.fst | 1 - ulib/FStar.Reflection.TermEq.fsti | 1 - ulib/FStar.SizeT.fst | 1 - ulib/FStar.TSet.fst | 1 - ulib/FStar.Tactics.V1.Derived.fst | 1 - ulib/FStar.Tactics.V2.Derived.fst | 1 - ulib/FStar.Vector.Properties.fst | 1 - ulib/LowStar.Buffer.fst | 4 ---- ulib/LowStar.BufferOps.fst | 4 ---- ulib/LowStar.BufferView.Up.fsti | 1 - ulib/LowStar.ConstBuffer.fst | 4 ---- ulib/LowStar.ImmutableBuffer.fst | 1 - ulib/LowStar.PrefixFreezableBuffer.fst | 4 ---- ulib/LowStar.PrefixFreezableBuffer.fsti | 2 -- ulib/LowStar.UninitializedBuffer.fst | 2 -- ulib/legacy/FStar.Buffer.fst | 1 - ulib/legacy/FStar.Pointer.Derived1.fst | 2 -- ulib/legacy/FStar.Pointer.Derived2.fst | 1 - ulib/legacy/FStar.Pointer.Derived2.fsti | 1 - ulib/legacy/FStar.Pointer.Derived3.fst | 1 - ulib/legacy/FStar.Pointer.Derived3.fsti | 1 - ulib/legacy/LowStar.BufferCompat.fst | 1 - ulib/ml/app/FStar_Bytes.ml | 1 - ulib/ml/plugin/FStarC_Tactics_V1_Builtins.ml | 5 ----- ulib/ml/plugin/FStarC_Tactics_V2_Builtins.ml | 6 ------ 162 files changed, 288 deletions(-) diff --git a/contrib/CoreCrypto/ml/Tests.ml b/contrib/CoreCrypto/ml/Tests.ml index ec339657f01..64d3eef17b8 100644 --- 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 index 84282b29f9d..aeeed7e4a22 100644 --- 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 index 484b88be181..c6fdcabd1e3 100644 --- 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 index 7a88fe184b2..9708e563e19 100644 --- 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 index be27113cfa6..d46a8085966 100644 --- 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 index 636871892d8..95cf68e76ae 100644 --- 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 index a1348330fd7..6a2c0d82eab 100644 --- 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 index 67464eb70ec..35b2340732d 100644 --- 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 index 774c1d875b9..822a768349c 100644 --- 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 index 5ede8b6c9df..3d94a2eae4d 100644 --- 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 index ea129b25710..cb2b5107e4d 100644 --- 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 index ded9680128d..a4dd0f95140 100644 --- 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 index 59849918b39..846bb815c85 100644 --- 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 index 79936304711..48941f6eef0 100644 --- 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 index 79f1784044f..fb2f1db1f44 100644 --- 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 index 87031c0f439..4b8a000c253 100644 --- 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 index c9d4450b4f6..465cff2a738 100644 --- 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 index 0665119566c..fc0771a2c29 100644 --- 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 index a29d0047f76..f053293b09d 100644 --- 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 index fa06e261c12..027e2f17e07 100644 --- 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 index ba347619a1a..0af2ae5e1a8 100644 --- 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 index d04badf406e..36a36ac2466 100644 --- 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 index 50a13dcabd7..1eddfa7fe25 100644 --- 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 index d1f1f29beaa..e06a8711571 100644 --- 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 index 8333f877352..cc4710903b1 100644 --- 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 index a2df8921030..11765c0bd11 100644 --- 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 index 98c98e72a61..4b318164438 100644 --- 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 index 45386d1f7c8..a79f992f65e 100644 --- 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 index ff7e740128f..65e1ca89297 100644 --- 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 index 8d47a335513..8d2f8959388 100644 --- 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 index 7fe0e086041..db74b3696c2 100644 --- 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 index cf442e36016..90349557257 100644 --- 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 index c04976ccaac..c476878896c 100644 --- 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 index b9e4b0fb831..e0fa2aa963f 100644 --- 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 index 32bff49fa4d..b7237f990de 100644 --- 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 index bfa5ac67dca..dc77087a492 100644 --- 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 index 7c5e0862941..31d8ce52603 100644 --- 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 index 0ebfdcb480a..2723ff41bb7 100644 --- 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 index 99ba2061b54..721d9772513 100644 --- 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 index 2c2baebc5c4..682e8fca50d 100644 --- 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 index d2f73511d6f..153321fa25e 100644 --- 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 index cc15db0a508..e8c9b7645fc 100644 --- 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 index 6634df87062..ea38357e562 100644 --- 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 index 922c71a8c83..92a4f38a2d8 100644 --- 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 diff --git a/examples/layeredeffects/everparse/LowParseWriters.LowParse.fst b/examples/layeredeffects/everparse/LowParseWriters.LowParse.fst index ab8741e8554..497ab95da42 100644 --- a/examples/layeredeffects/everparse/LowParseWriters.LowParse.fst +++ b/examples/layeredeffects/everparse/LowParseWriters.LowParse.fst @@ -1,7 +1,6 @@ module LowParseWriters.LowParse module LP = LowParse.Low.Combinators -module LPI = LowParse.Low.Int module U8 = FStar.UInt8 module Seq = FStar.Seq diff --git a/examples/layeredeffects/everparse/tls/Negotiation.Writers.Aux.fsti b/examples/layeredeffects/everparse/tls/Negotiation.Writers.Aux.fsti index 2edea3bae09..d3070f15a50 100644 --- a/examples/layeredeffects/everparse/tls/Negotiation.Writers.Aux.fsti +++ b/examples/layeredeffects/everparse/tls/Negotiation.Writers.Aux.fsti @@ -3,7 +3,6 @@ module Negotiation.Writers.Aux (* TODO: all of these, along with their implementations in the .fst, should be automatically generated by QuackyDucky *) module LWP = LowParseWriters.Parsers -module LPI = LowParse.Low.Int val valid_pskBinderEntry_intro : LWP.valid_rewrite_t (LWP.parse_vlbytes 32ul 255ul) Parsers.PskBinderEntry.lwp_pskBinderEntry (fun _ -> True) (fun x -> x) diff --git a/examples/layeredeffects/everparse/tls/Negotiation.Writers.Aux2.fsti b/examples/layeredeffects/everparse/tls/Negotiation.Writers.Aux2.fsti index c840e26018f..39888ddef13 100644 --- a/examples/layeredeffects/everparse/tls/Negotiation.Writers.Aux2.fsti +++ b/examples/layeredeffects/everparse/tls/Negotiation.Writers.Aux2.fsti @@ -3,7 +3,6 @@ module Negotiation.Writers.Aux2 (* TODO: all of these, along with their implementations in the .fst, should be automatically generated by QuackyDucky *) module LWP = LowParseWriters.Parsers -module LPI = LowParse.Low.Int val valid_rewrite_constr_clientHelloExtension_CHE_pre_shared_key : LWP.valid_rewrite_t (Parsers.ExtensionType.lwp_extensionType `LWP.parse_pair` Parsers.ClientHelloExtension.lwp_clientHelloExtension_CHE_pre_shared_key) diff --git a/examples/layeredeffects/everparse/tls/Negotiation.Writers.NoHoare.Aux.fst b/examples/layeredeffects/everparse/tls/Negotiation.Writers.NoHoare.Aux.fst index df821088ae3..618b7535611 100644 --- a/examples/layeredeffects/everparse/tls/Negotiation.Writers.NoHoare.Aux.fst +++ b/examples/layeredeffects/everparse/tls/Negotiation.Writers.NoHoare.Aux.fst @@ -5,7 +5,6 @@ include Negotiation.Writers.Aux module LWP = LowParseWriters.Parsers module LWPS = LowParseWriters.NoHoare.Parsers -module LPI = LowParse.Low.Int let valid_pskBinderEntry_intro' = LWPS.tvalid_rewrite_of_evalid_rewrite valid_pskBinderEntry_intro diff --git a/examples/layeredeffects/everparse/tls/Negotiation.Writers.NoHoare.Aux2.fst b/examples/layeredeffects/everparse/tls/Negotiation.Writers.NoHoare.Aux2.fst index 8aaf3723a08..9beae97d372 100644 --- a/examples/layeredeffects/everparse/tls/Negotiation.Writers.NoHoare.Aux2.fst +++ b/examples/layeredeffects/everparse/tls/Negotiation.Writers.NoHoare.Aux2.fst @@ -5,7 +5,6 @@ include Negotiation.Writers.Aux2 module LWP = LowParseWriters.Parsers module LWPS = LowParseWriters.NoHoare.Parsers -module LPI = LowParse.Low.Int inline_for_extraction noextract diff --git a/examples/low-mitls-experiments/HSL.fsti b/examples/low-mitls-experiments/HSL.fsti index bca2cc2b1d2..c3ac4cd72cb 100644 --- a/examples/low-mitls-experiments/HSL.fsti +++ b/examples/low-mitls-experiments/HSL.fsti @@ -29,7 +29,6 @@ open FStar.HyperStack.ST module Mods = LowStar.Modifies module Buffer = LowStar.Buffer -module ST = FStar.HyperStack.ST type u32 = UInt32.t diff --git a/examples/low-mitls-experiments/ImmutableBuffer.fst b/examples/low-mitls-experiments/ImmutableBuffer.fst index 3cec9945f0f..61704d526d4 100644 --- a/examples/low-mitls-experiments/ImmutableBuffer.fst +++ b/examples/low-mitls-experiments/ImmutableBuffer.fst @@ -19,7 +19,6 @@ module B = LowStar.Buffer module HS = FStar.HyperStack module HST = FStar.HyperStack.ST module Seq = FStar.Seq -module U32 = FStar.UInt32 module IB = LowStar.ImmutableBuffer diff --git a/examples/miniparse/MiniParse.Impl.List.fst b/examples/miniparse/MiniParse.Impl.List.fst index df4448cd990..ae66e410de4 100644 --- a/examples/miniparse/MiniParse.Impl.List.fst +++ b/examples/miniparse/MiniParse.Impl.List.fst @@ -18,7 +18,6 @@ include MiniParse.Spec.List include MiniParse.Impl.Base include MiniParse.Impl.Combinators // for seq_append_slice -module U8 = FStar.UInt8 module U32 = FStar.UInt32 module HS = FStar.HyperStack module HST = FStar.HyperStack.ST diff --git a/examples/miniparse/MiniParse.Impl.TSum.fst b/examples/miniparse/MiniParse.Impl.TSum.fst index 0422e3b9b2c..ce508c16377 100644 --- a/examples/miniparse/MiniParse.Impl.TSum.fst +++ b/examples/miniparse/MiniParse.Impl.TSum.fst @@ -18,7 +18,6 @@ include MiniParse.Impl.Combinators include MiniParse.Spec.TSum module B = LowStar.Buffer -module M = LowStar.ModifiesPat module U32 = FStar.UInt32 module HST = FStar.HyperStack.ST diff --git a/examples/miniparse/MiniParse.Spec.Base.fst b/examples/miniparse/MiniParse.Spec.Base.fst index 39e0f1ed165..752a5825ceb 100644 --- a/examples/miniparse/MiniParse.Spec.Base.fst +++ b/examples/miniparse/MiniParse.Spec.Base.fst @@ -17,7 +17,6 @@ module MiniParse.Spec.Base module Seq = FStar.Seq module U8 = FStar.UInt8 -module U32 = FStar.UInt32 inline_for_extraction type byte = U8.t diff --git a/examples/miniparse/MiniParse.Spec.Combinators.fst b/examples/miniparse/MiniParse.Spec.Combinators.fst index 09b4172cfe9..73e96e1af66 100644 --- a/examples/miniparse/MiniParse.Spec.Combinators.fst +++ b/examples/miniparse/MiniParse.Spec.Combinators.fst @@ -17,8 +17,6 @@ module MiniParse.Spec.Combinators include MiniParse.Spec.Base module Seq = FStar.Seq -module U8 = FStar.UInt8 -module U32 = FStar.UInt32 (** Constant-size parsers *) diff --git a/examples/miniparse/MiniParse.Spec.List.fst b/examples/miniparse/MiniParse.Spec.List.fst index b5dca78da8d..88173a55500 100644 --- a/examples/miniparse/MiniParse.Spec.List.fst +++ b/examples/miniparse/MiniParse.Spec.List.fst @@ -18,8 +18,6 @@ include MiniParse.Spec.Combinators // for seq_slice_append_l module Seq = FStar.Seq module L = FStar.List.Tot -module U32 = FStar.UInt32 -module Classical = FStar.Classical let nlist_nil_unique (t: Type) (l: nlist 0 t) : Lemma (l == nlist_nil) = () diff --git a/examples/miniparse/MiniParse.Spec.List.fsti b/examples/miniparse/MiniParse.Spec.List.fsti index 36ec7116b70..14c79ec0d8f 100644 --- a/examples/miniparse/MiniParse.Spec.List.fsti +++ b/examples/miniparse/MiniParse.Spec.List.fsti @@ -18,7 +18,6 @@ include MiniParse.Spec.Combinators // for seq_slice_append_l module Seq = FStar.Seq module L = FStar.List.Tot -module U32 = FStar.UInt32 module Classical = FStar.Classical // inline_for_extraction diff --git a/examples/miniparse/MiniParse.Tac.Impl.fst b/examples/miniparse/MiniParse.Tac.Impl.fst index fb71113fa28..6328caf1677 100644 --- a/examples/miniparse/MiniParse.Tac.Impl.fst +++ b/examples/miniparse/MiniParse.Tac.Impl.fst @@ -21,7 +21,6 @@ include MiniParse.Impl.List include MiniParse.Spec.TEnum module T = FStar.Tactics.V2 -module L = FStar.List.Tot module TS = MiniParse.Tac.Spec module U32 = FStar.UInt32 diff --git a/examples/miniparse/MiniParseExample2.fst b/examples/miniparse/MiniParseExample2.fst index 5ede3ac6e25..baad33a9b71 100644 --- a/examples/miniparse/MiniParseExample2.fst +++ b/examples/miniparse/MiniParseExample2.fst @@ -16,7 +16,6 @@ module MiniParseExample2 open MiniParse.Spec.TSum -module T = FStar.Tactics.V2 module U8 = FStar.UInt8 noeq diff --git a/examples/native_tactics/Imp.List.fst b/examples/native_tactics/Imp.List.fst index b348ac35fed..a7de17fb79b 100644 --- a/examples/native_tactics/Imp.List.fst +++ b/examples/native_tactics/Imp.List.fst @@ -32,7 +32,6 @@ type inst = | Seq : prog -> inst and prog = list inst -module L = FStar.List.Tot let rec size : inst -> pos = function | Add _ _ _ diff --git a/examples/old/Buffers.fst b/examples/old/Buffers.fst index 2eafade3740..f832f6d3c29 100644 --- a/examples/old/Buffers.fst +++ b/examples/old/Buffers.fst @@ -28,7 +28,6 @@ open FStar.Integers open FStar.HyperStack.ST -module HS = FStar.HyperStack module B = LowStar.Buffer diff --git a/examples/old/Setoids.Crypto.fst b/examples/old/Setoids.Crypto.fst index 1d4f541e149..ec5854b0edd 100644 --- a/examples/old/Setoids.Crypto.fst +++ b/examples/old/Setoids.Crypto.fst @@ -1,5 +1,4 @@ module Setoids.Crypto -module L = Setoids open FStar.Integers open FStar.Map open Setoids diff --git a/examples/old/tls-record-layer/LowCProvider/Tests.ml b/examples/old/tls-record-layer/LowCProvider/Tests.ml index 2d1aca12584..fd3ea786ecf 100644 --- a/examples/old/tls-record-layer/LowCProvider/Tests.ml +++ b/examples/old/tls-record-layer/LowCProvider/Tests.ml @@ -1,5 +1,4 @@ (* The original "Bytes" module from OCaml. *) -module B = Bytes (* This brings [Platform.Bytes] into scope. *) open CoreCrypto diff --git a/examples/old/tls-record-layer/crypto/Crypto.AEAD.Chacha20Poly1305.fst b/examples/old/tls-record-layer/crypto/Crypto.AEAD.Chacha20Poly1305.fst index ca70aa5679f..b3e3111ef31 100644 --- a/examples/old/tls-record-layer/crypto/Crypto.AEAD.Chacha20Poly1305.fst +++ b/examples/old/tls-record-layer/crypto/Crypto.AEAD.Chacha20Poly1305.fst @@ -25,7 +25,6 @@ open Crypto.Indexing //16-10-02 THIS FILE IS USED ONLY BY AEAD-TEST; use Crypto.AEAD instead. // now hiding the 1-time MAC state & implementation -module Spec = Crypto.Symmetric.Poly1305.Spec module MAC = Crypto.Symmetric.Poly1305.MAC module Bytes = Crypto.Symmetric.Bytes diff --git a/examples/old/tls-record-layer/crypto/Crypto.AEAD.Decrypt.fst b/examples/old/tls-record-layer/crypto/Crypto.AEAD.Decrypt.fst index e53a5a01672..4265cff3355 100644 --- a/examples/old/tls-record-layer/crypto/Crypto.AEAD.Decrypt.fst +++ b/examples/old/tls-record-layer/crypto/Crypto.AEAD.Decrypt.fst @@ -29,16 +29,13 @@ open Crypto.Symmetric.PRF open Crypto.AEAD.Encoding open Crypto.AEAD.Invariant -module HH = FStar.HyperHeap module HS = FStar.HyperStack -module ST = FStar.HyperStack.ST module MAC = Crypto.Symmetric.MAC module CMA = Crypto.Symmetric.UF1CMA module Plain = Crypto.Plain module Cipher = Crypto.Symmetric.Cipher module PRF = Crypto.Symmetric.PRF module Dexor = Crypto.AEAD.EnxorDexor -module Encoding = Crypto.AEAD.Encoding module EncodingWrapper = Crypto.AEAD.Wrappers.Encoding module CMAWrapper = Crypto.AEAD.Wrappers.CMA module PRF_MAC = Crypto.AEAD.Wrappers.PRF diff --git a/examples/old/tls-record-layer/crypto/Crypto.AEAD.Encoding.fst b/examples/old/tls-record-layer/crypto/Crypto.AEAD.Encoding.fst index e2c1db26f67..acdcefdc9b9 100644 --- a/examples/old/tls-record-layer/crypto/Crypto.AEAD.Encoding.fst +++ b/examples/old/tls-record-layer/crypto/Crypto.AEAD.Encoding.fst @@ -38,8 +38,6 @@ module ST = FStar.HyperStack.ST module MAC = Crypto.Symmetric.MAC module CMA = Crypto.Symmetric.UF1CMA -module Cipher = Crypto.Symmetric.Cipher -module PRF = Crypto.Symmetric.PRF type region = rgn:HH.rid {HS.is_eternal_region rgn} diff --git a/examples/old/tls-record-layer/crypto/Crypto.AEAD.Encrypt.Aux.fst b/examples/old/tls-record-layer/crypto/Crypto.AEAD.Encrypt.Aux.fst index 94a1b30e577..3356267afa5 100644 --- a/examples/old/tls-record-layer/crypto/Crypto.AEAD.Encrypt.Aux.fst +++ b/examples/old/tls-record-layer/crypto/Crypto.AEAD.Encrypt.Aux.fst @@ -30,7 +30,6 @@ open Crypto.AEAD.Invariant module Cipher = Crypto.Symmetric.Cipher module PRF = Crypto.Symmetric.PRF module Plain = Crypto.Plain -module Invariant = Crypto.AEAD.Invariant module HH = FStar.HyperHeap module HS = FStar.HyperStack module CMA = Crypto.Symmetric.UF1CMA diff --git a/examples/old/tls-record-layer/crypto/Crypto.AEAD.Encrypt.Ideal.Invariant.fst b/examples/old/tls-record-layer/crypto/Crypto.AEAD.Encrypt.Ideal.Invariant.fst index 6cd7121944a..ba3085d3ff7 100644 --- a/examples/old/tls-record-layer/crypto/Crypto.AEAD.Encrypt.Ideal.Invariant.fst +++ b/examples/old/tls-record-layer/crypto/Crypto.AEAD.Encrypt.Ideal.Invariant.fst @@ -31,11 +31,8 @@ open Crypto.AEAD.Encrypt.Invariant module HS = FStar.HyperStack -module MAC = Crypto.Symmetric.MAC module PRF = Crypto.Symmetric.PRF -module CMA = Crypto.Symmetric.UF1CMA module Cipher = Crypto.Symmetric.Cipher -module BufferUtils = Crypto.AEAD.BufferUtils #reset-options "--z3rlimit 100 --initial_fuel 0 --max_fuel 0 --initial_ifuel 0 --max_ifuel 0" let safeMac_ideal_writes diff --git a/examples/old/tls-record-layer/crypto/Crypto.AEAD.Encrypt.Invariant.fst b/examples/old/tls-record-layer/crypto/Crypto.AEAD.Encrypt.Invariant.fst index f67f7521b8d..c1c5fc4886c 100644 --- a/examples/old/tls-record-layer/crypto/Crypto.AEAD.Encrypt.Invariant.fst +++ b/examples/old/tls-record-layer/crypto/Crypto.AEAD.Encrypt.Invariant.fst @@ -28,10 +28,8 @@ open Flag open Crypto.AEAD.Encoding open Crypto.Symmetric.PRF -module HH = FStar.HyperHeap module HS = FStar.HyperStack -module MAC = Crypto.Symmetric.MAC module CMA = Crypto.Symmetric.UF1CMA module Cipher = Crypto.Symmetric.Cipher module PRF = Crypto.Symmetric.PRF diff --git a/examples/old/tls-record-layer/crypto/Crypto.AEAD.Encrypt.fst b/examples/old/tls-record-layer/crypto/Crypto.AEAD.Encrypt.fst index 08debf27e5d..620c357d14a 100644 --- a/examples/old/tls-record-layer/crypto/Crypto.AEAD.Encrypt.fst +++ b/examples/old/tls-record-layer/crypto/Crypto.AEAD.Encrypt.fst @@ -33,7 +33,6 @@ open Crypto.AEAD.Enxor.Invariant open Crypto.AEAD.MAC_Wrapper.Invariant open Crypto.AEAD.Encrypt.Ideal.Invariant -module HH = FStar.HyperHeap module HS = FStar.HyperStack module ST = FStar.HyperStack.ST module MAC = Crypto.Symmetric.MAC @@ -43,7 +42,6 @@ module Cipher = Crypto.Symmetric.Cipher module PRF = Crypto.Symmetric.PRF module Enxor = Crypto.AEAD.EnxorDexor module PRF_MAC = Crypto.AEAD.Wrappers.PRF -module Encoding = Crypto.AEAD.Encoding module EncodingWrapper = Crypto.AEAD.Wrappers.Encoding module CMAWrapper = Crypto.AEAD.Wrappers.CMA diff --git a/examples/old/tls-record-layer/crypto/Crypto.AEAD.Enxor.Invariant.fst b/examples/old/tls-record-layer/crypto/Crypto.AEAD.Enxor.Invariant.fst index cd3f1279fde..aa891d08958 100644 --- a/examples/old/tls-record-layer/crypto/Crypto.AEAD.Enxor.Invariant.fst +++ b/examples/old/tls-record-layer/crypto/Crypto.AEAD.Enxor.Invariant.fst @@ -28,11 +28,8 @@ open Flag open Crypto.AEAD.Encoding open Crypto.Symmetric.PRF -module HH = FStar.HyperHeap module HS = FStar.HyperStack -module MAC = Crypto.Symmetric.MAC -module CMA = Crypto.Symmetric.UF1CMA module Cipher = Crypto.Symmetric.Cipher module PRF = Crypto.Symmetric.PRF module Plain = Crypto.Plain diff --git a/examples/old/tls-record-layer/crypto/Crypto.AEAD.EnxorDexor.fst b/examples/old/tls-record-layer/crypto/Crypto.AEAD.EnxorDexor.fst index e506afa4072..042733ec85c 100644 --- a/examples/old/tls-record-layer/crypto/Crypto.AEAD.EnxorDexor.fst +++ b/examples/old/tls-record-layer/crypto/Crypto.AEAD.EnxorDexor.fst @@ -32,7 +32,6 @@ open Crypto.AEAD.Encrypt.Invariant module Cipher = Crypto.Symmetric.Cipher module PRF = Crypto.Symmetric.PRF module Plain = Crypto.Plain -module Invariant = Crypto.AEAD.Invariant module HH = FStar.HyperHeap module HS = FStar.HyperStack module ST = FStar.HyperStack.ST diff --git a/examples/old/tls-record-layer/crypto/Crypto.AEAD.Invariant.fst b/examples/old/tls-record-layer/crypto/Crypto.AEAD.Invariant.fst index a6efbb7bc79..a9fbbd13888 100644 --- a/examples/old/tls-record-layer/crypto/Crypto.AEAD.Invariant.fst +++ b/examples/old/tls-record-layer/crypto/Crypto.AEAD.Invariant.fst @@ -35,7 +35,6 @@ open FStar.HyperStack.ST module HH = FStar.HyperHeap module HS = FStar.HyperStack -module ST = FStar.HyperStack.ST module MAC = Crypto.Symmetric.MAC module CMA = Crypto.Symmetric.UF1CMA diff --git a/examples/old/tls-record-layer/crypto/Crypto.AEAD.MAC_Wrapper.Invariant.fst b/examples/old/tls-record-layer/crypto/Crypto.AEAD.MAC_Wrapper.Invariant.fst index 595c1e5439e..312f2b745ff 100644 --- a/examples/old/tls-record-layer/crypto/Crypto.AEAD.MAC_Wrapper.Invariant.fst +++ b/examples/old/tls-record-layer/crypto/Crypto.AEAD.MAC_Wrapper.Invariant.fst @@ -28,7 +28,6 @@ open Flag open Crypto.AEAD.Encoding open Crypto.Symmetric.PRF -module HH = FStar.HyperHeap module HS = FStar.HyperStack module MAC = Crypto.Symmetric.MAC diff --git a/examples/old/tls-record-layer/crypto/Crypto.AEAD.Wrappers.CMA.fst b/examples/old/tls-record-layer/crypto/Crypto.AEAD.Wrappers.CMA.fst index 4b3a35c598e..05b805e8557 100644 --- a/examples/old/tls-record-layer/crypto/Crypto.AEAD.Wrappers.CMA.fst +++ b/examples/old/tls-record-layer/crypto/Crypto.AEAD.Wrappers.CMA.fst @@ -33,9 +33,7 @@ module Cipher = Crypto.Symmetric.Cipher module PRF = Crypto.Symmetric.PRF module Plain = Crypto.Plain module Invariant = Crypto.AEAD.Invariant -module HH = FStar.HyperHeap module HS = FStar.HyperStack -module ST = FStar.HyperStack.ST module CMA = Crypto.Symmetric.UF1CMA module Seq = FStar.Seq module MAC = Crypto.Symmetric.MAC diff --git a/examples/old/tls-record-layer/crypto/Crypto.AEAD.Wrappers.Encoding.fst b/examples/old/tls-record-layer/crypto/Crypto.AEAD.Wrappers.Encoding.fst index 78b609966e1..1174abe8c08 100644 --- a/examples/old/tls-record-layer/crypto/Crypto.AEAD.Wrappers.Encoding.fst +++ b/examples/old/tls-record-layer/crypto/Crypto.AEAD.Wrappers.Encoding.fst @@ -31,9 +31,7 @@ open Crypto.Symmetric.Bytes open Crypto.Plain open Flag -module HH = FStar.HyperHeap module HS = FStar.HyperStack -module ST = FStar.HyperStack.ST module MAC = Crypto.Symmetric.MAC module CMA = Crypto.Symmetric.UF1CMA diff --git a/examples/old/tls-record-layer/crypto/Crypto.AEAD.Wrappers.PRF.fst b/examples/old/tls-record-layer/crypto/Crypto.AEAD.Wrappers.PRF.fst index e241025d0a3..e810425a9d9 100644 --- a/examples/old/tls-record-layer/crypto/Crypto.AEAD.Wrappers.PRF.fst +++ b/examples/old/tls-record-layer/crypto/Crypto.AEAD.Wrappers.PRF.fst @@ -31,7 +31,6 @@ open Crypto.AEAD.Invariant open Crypto.AEAD.Encrypt.Invariant module HS = FStar.HyperStack -module ST = FStar.HyperStack.ST module MAC = Crypto.Symmetric.MAC module PRF = Crypto.Symmetric.PRF diff --git a/examples/old/tls-record-layer/crypto/Crypto.AEAD.fst b/examples/old/tls-record-layer/crypto/Crypto.AEAD.fst index 1aca57dfe90..8a91642b089 100644 --- a/examples/old/tls-record-layer/crypto/Crypto.AEAD.fst +++ b/examples/old/tls-record-layer/crypto/Crypto.AEAD.fst @@ -41,18 +41,9 @@ open Crypto.AEAD.Encoding open Crypto.AEAD.Invariant (* open Crypto.AEAD.Wrappers *) -module HH = FStar.HyperHeap -module HS = FStar.HyperStack -module ST = FStar.HyperStack.ST module MAC = Crypto.Symmetric.MAC module CMA = Crypto.Symmetric.UF1CMA -module Plain = Crypto.Plain -module Cipher = Crypto.Symmetric.Cipher module PRF = Crypto.Symmetric.PRF -module Enxor = Crypto.AEAD.EnxorDexor -module Dexor = Crypto.AEAD.EnxorDexor -module PRF_MAC = Crypto.AEAD.Wrappers.PRF -module Encoding = Crypto.AEAD.Encoding val gen: i:id -> diff --git a/examples/old/tls-record-layer/crypto/Crypto.KrmlTest.fst b/examples/old/tls-record-layer/crypto/Crypto.KrmlTest.fst index 7240ae29579..758ff67a844 100644 --- a/examples/old/tls-record-layer/crypto/Crypto.KrmlTest.fst +++ b/examples/old/tls-record-layer/crypto/Crypto.KrmlTest.fst @@ -42,19 +42,12 @@ open Buffer open Flag module HH = FStar.HyperHeap -module HS = FStar.HyperStack -module ST = FStar.HyperStack.ST module Plain = Crypto.Plain -module MAC = Crypto.Symmetric.MAC module Cipher = Crypto.Symmetric.Cipher -module PRF = Crypto.Symmetric.PRF module AE = Crypto.AEAD module AETypes = Crypto.AEAD.Invariant -module D = Crypto.AEAD.Decrypt -module E = Crypto.AEAD.Encrypt -module L = FStar.List.Tot #set-options "--admit_smt_queries true" diff --git a/examples/old/tls-record-layer/crypto/Crypto.Symmetric.AES.fst b/examples/old/tls-record-layer/crypto/Crypto.Symmetric.AES.fst index 943167ed5ca..c82d92a1d47 100644 --- a/examples/old/tls-record-layer/crypto/Crypto.Symmetric.AES.fst +++ b/examples/old/tls-record-layer/crypto/Crypto.Symmetric.AES.fst @@ -31,11 +31,8 @@ open FStar.Int.Cast open FStar.Buffer (* Module abbreviations *) -module HH = FStar.HyperHeap -module HS = FStar.HyperStack module ST = FStar.HyperStack.ST -module U8 = FStar.UInt8 module U32 = FStar.UInt32 module H8 = FStar.UInt8 module H32 = FStar.UInt32 diff --git a/examples/old/tls-record-layer/crypto/Crypto.Symmetric.AES128.fst b/examples/old/tls-record-layer/crypto/Crypto.Symmetric.AES128.fst index 5abafbb128a..6d87e69910d 100644 --- a/examples/old/tls-record-layer/crypto/Crypto.Symmetric.AES128.fst +++ b/examples/old/tls-record-layer/crypto/Crypto.Symmetric.AES128.fst @@ -27,11 +27,8 @@ open FStar.Int.Cast open FStar.Buffer (* Module abbreviations *) -module HH = FStar.HyperHeap -module HS = FStar.HyperStack module ST = FStar.HyperStack.ST -module U8 = FStar.UInt8 module U32 = FStar.UInt32 module H8 = FStar.UInt8 module H32 = FStar.UInt32 diff --git a/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Bytes.fst b/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Bytes.fst index 0c6e27b4d9e..a4338e66c1f 100644 --- a/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Bytes.fst +++ b/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Bytes.fst @@ -349,7 +349,6 @@ let rec uint32_be len n = // ----- lower-level stuff -module U8 = FStar.UInt8 let u8 = UInt8.t let u32 = UInt32.t diff --git a/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Chacha20.fst b/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Chacha20.fst index ae98c79999b..6194f22c4cf 100644 --- a/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Chacha20.fst +++ b/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Chacha20.fst @@ -31,8 +31,6 @@ open FStar.HyperStack.ST open FStar.Buffer open Buffer.Utils -module HS = FStar.HyperStack -module ST = FStar.HyperStack.ST type u64 = FStar.UInt64.t diff --git a/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Cipher.fst b/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Cipher.fst index 09f524f4527..79c7972c660 100644 --- a/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Cipher.fst +++ b/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Cipher.fst @@ -23,8 +23,6 @@ open FStar.HyperStack.ST open FStar.Buffer open Buffer.Utils -module HH = FStar.HyperHeap -module HS = FStar.HyperStack module ST = FStar.HyperStack.ST open FStar.UInt32 diff --git a/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part1.fst b/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part1.fst index adb660b31ca..69288527379 100644 --- a/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part1.fst +++ b/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part1.fst @@ -32,7 +32,6 @@ open Crypto.Symmetric.Poly1305.Bigint module U32 = FStar.UInt32 module U64 = FStar.UInt64 -module HS = FStar.HyperStack val prime: p:erased pos{reveal p = Crypto.Symmetric.Poly1305.Spec.p_1305} let prime = hide (Crypto.Symmetric.Poly1305.Spec.p_1305) diff --git a/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part2.fst b/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part2.fst index 13b06e8d4f2..4186311fd69 100644 --- a/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part2.fst +++ b/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part2.fst @@ -32,9 +32,6 @@ open Crypto.Symmetric.Poly1305.Bigint open Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part1 -module U32 = FStar.UInt32 -module U64 = FStar.UInt64 -module HS = FStar.HyperStack #reset-options "--z3rlimit 20 --initial_fuel 0 --max_fuel 0" diff --git a/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part3.fst b/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part3.fst index d5183318266..54122dae49e 100644 --- a/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part3.fst +++ b/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part3.fst @@ -32,9 +32,6 @@ open Crypto.Symmetric.Poly1305.Bigint open Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part1 open Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part2 -module U32 = FStar.UInt32 -module U64 = FStar.UInt64 -module HS = FStar.HyperStack #reset-options "--z3rlimit 5 --initial_fuel 0 --max_fuel 0" diff --git a/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part5.fst b/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part5.fst index eb061cd5253..aaa87184b32 100644 --- a/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part5.fst +++ b/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part5.fst @@ -34,7 +34,6 @@ open Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part2 open Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part3 open Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part4 -module U64 = FStar.UInt64 #reset-options "--z3rlimit 20 --initial_fuel 0 --max_fuel 0" diff --git a/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part6.fst b/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part6.fst index 5a114d0a369..790aa707efb 100644 --- a/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part6.fst +++ b/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part6.fst @@ -32,7 +32,6 @@ open Crypto.Symmetric.Poly1305.Bigint module U32 = FStar.UInt32 module U64 = FStar.UInt64 -module HS = FStar.HyperStack open FStar.Buffer.Quantifiers open Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part1 diff --git a/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.Bignum.fst b/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.Bignum.fst index 8b63a4795a0..67cdf4f92ca 100644 --- a/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.Bignum.fst +++ b/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.Bignum.fst @@ -33,7 +33,6 @@ open Crypto.Symmetric.Poly1305.Bigint module U32 = FStar.UInt32 module U64 = FStar.UInt64 -module HS = FStar.HyperStack module ST = FStar.HyperStack.ST open FStar.Buffer.Quantifiers diff --git a/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.Spec.fst b/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.Spec.fst index c9a53d9cafe..77bd4d78cfe 100644 --- a/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.Spec.fst +++ b/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.Spec.fst @@ -34,8 +34,6 @@ open FStar.Math.Lemmas open Crypto.Symmetric.Bytes module U8 = FStar.UInt8 -module U32 = FStar.UInt32 -module U64 = FStar.UInt64 (** Poly1305 prime *) let p_1305: p:nat{pow2 128 < p} = diff --git a/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.fst b/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.fst index ad83e64b4b1..fbe851df1e1 100644 --- a/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.fst +++ b/examples/old/tls-record-layer/crypto/Crypto.Symmetric.Poly1305.fst @@ -45,7 +45,6 @@ open Flag module U8 = FStar.UInt8 module U32 = FStar.UInt32 module U64 = FStar.UInt64 -module HS = FStar.HyperStack module ST = FStar.HyperStack.ST (* 2016-11-22: we now forbid opening the current module name as a diff --git a/examples/old/tls-record-layer/crypto/Crypto.WIP.fst b/examples/old/tls-record-layer/crypto/Crypto.WIP.fst index a196e57c7d6..4433ee6a1a0 100644 --- a/examples/old/tls-record-layer/crypto/Crypto.WIP.fst +++ b/examples/old/tls-record-layer/crypto/Crypto.WIP.fst @@ -38,15 +38,8 @@ open Crypto.AEAD.Lemmas.Part2 open Crypto.AEAD.BufferUtils open Crypto.AEAD -module HH = FStar.HyperHeap -module HS = FStar.HyperStack -module CMA = Crypto.Symmetric.UF1CMA -module MAC = Crypto.Symmetric.MAC -module Cipher = Crypto.Symmetric.Cipher -module PRF = Crypto.Symmetric.PRF -module Plain = Crypto.Plain diff --git a/examples/old/tls-record-layer/crypto/stale/Curve.AddAndDouble.fst b/examples/old/tls-record-layer/crypto/stale/Curve.AddAndDouble.fst index c67b32d4213..3874ad2c4f0 100644 --- a/examples/old/tls-record-layer/crypto/stale/Curve.AddAndDouble.fst +++ b/examples/old/tls-record-layer/crypto/stale/Curve.AddAndDouble.fst @@ -27,9 +27,7 @@ open Curve.Bigint open Curve.Bignum open Curve.Point -module U8 = FStar.UInt8 module U32 = FStar.UInt32 -module U64 = FStar.UInt64 module U128 = FStar.UInt128 module HS = FStar.HyperStack diff --git a/examples/old/tls-record-layer/crypto/stale/Curve.Bignum.fst b/examples/old/tls-record-layer/crypto/stale/Curve.Bignum.fst index 74b51009b6e..60214d1852c 100644 --- a/examples/old/tls-record-layer/crypto/stale/Curve.Bignum.fst +++ b/examples/old/tls-record-layer/crypto/stale/Curve.Bignum.fst @@ -26,9 +26,7 @@ open Math.Field open Curve.Parameters open Curve.Bigint -module U8 = FStar.UInt8 module U32 = FStar.UInt32 -module U64 = FStar.UInt64 module U128 = FStar.UInt128 module HS = FStar.HyperStack diff --git a/examples/old/tls-record-layer/crypto/stale/Curve.Fdifference.fst b/examples/old/tls-record-layer/crypto/stale/Curve.Fdifference.fst index a810e66d92f..87d519d1ebb 100644 --- a/examples/old/tls-record-layer/crypto/stale/Curve.Fdifference.fst +++ b/examples/old/tls-record-layer/crypto/stale/Curve.Fdifference.fst @@ -27,9 +27,7 @@ open Curve.Bigint #set-options "--admit_smt_queries true" -module U8 = FStar.UInt8 module U32 = FStar.UInt32 -module U64 = FStar.UInt64 let op_Plus_Bar = U32.add let op_Subtraction_Bar = U32.sub diff --git a/examples/old/tls-record-layer/crypto/stale/Curve.Fproduct.fst b/examples/old/tls-record-layer/crypto/stale/Curve.Fproduct.fst index d5bef0f90a4..f861caa3b8e 100644 --- a/examples/old/tls-record-layer/crypto/stale/Curve.Fproduct.fst +++ b/examples/old/tls-record-layer/crypto/stale/Curve.Fproduct.fst @@ -27,10 +27,8 @@ open Curve.Bigint #set-options "--admit_smt_queries true" -module U8 = FStar.UInt8 module U32 = FStar.UInt32 module U64 = FStar.UInt64 -module U128 = FStar.UInt128 let w: u32 -> Tot int = U32.v let vv: u64 -> Tot int = U64.v diff --git a/examples/old/tls-record-layer/crypto/stale/Curve.Fscalar.fst b/examples/old/tls-record-layer/crypto/stale/Curve.Fscalar.fst index 0df547815b8..e70bdc40e01 100644 --- a/examples/old/tls-record-layer/crypto/stale/Curve.Fscalar.fst +++ b/examples/old/tls-record-layer/crypto/stale/Curve.Fscalar.fst @@ -27,9 +27,7 @@ open Curve.Bigint #set-options "--admit_smt_queries true" -module U8 = FStar.UInt8 module U32 = FStar.UInt32 -module U64 = FStar.UInt64 module U128 = FStar.UInt128 let w: u32 -> Tot int = U32.v diff --git a/examples/old/tls-record-layer/crypto/stale/Curve.Fsum.fst b/examples/old/tls-record-layer/crypto/stale/Curve.Fsum.fst index 2de254be022..d5d6db54688 100644 --- a/examples/old/tls-record-layer/crypto/stale/Curve.Fsum.fst +++ b/examples/old/tls-record-layer/crypto/stale/Curve.Fsum.fst @@ -27,9 +27,7 @@ open Curve.Bigint #set-options "--admit_smt_queries true" -module U8 = FStar.UInt8 module U32 = FStar.UInt32 -module U64 = FStar.UInt64 abstract type willNotOverflow (h:heap) (a:bigint{live h a /\ length a >= norm_length}) diff --git a/examples/old/tls-record-layer/crypto/stale/Curve.FsumWide.fst b/examples/old/tls-record-layer/crypto/stale/Curve.FsumWide.fst index 94f92490d7e..9b477310ce1 100644 --- a/examples/old/tls-record-layer/crypto/stale/Curve.FsumWide.fst +++ b/examples/old/tls-record-layer/crypto/stale/Curve.FsumWide.fst @@ -27,10 +27,7 @@ open Curve.Bigint #set-options "--admit_smt_queries true" -module U8 = FStar.UInt8 module U32 = FStar.UInt32 -module U64 = FStar.UInt64 -module U128 = FStar.UInt128 let u32 = U32.t let op_Plus_Bar = U32.add diff --git a/examples/old/tls-record-layer/crypto/stale/Curve.Modulo.fst b/examples/old/tls-record-layer/crypto/stale/Curve.Modulo.fst index 0361c17619f..3075d3ba2ed 100644 --- a/examples/old/tls-record-layer/crypto/stale/Curve.Modulo.fst +++ b/examples/old/tls-record-layer/crypto/stale/Curve.Modulo.fst @@ -28,7 +28,6 @@ open Math.Field open Curve.Parameters open Curve.Bigint -module U8 = FStar.UInt8 module U32 = FStar.UInt32 module U64 = FStar.UInt64 module U128 = FStar.UInt128 diff --git a/examples/old/tls-record-layer/crypto/stale/Curve.Point.fst b/examples/old/tls-record-layer/crypto/stale/Curve.Point.fst index 6b2a1c4422f..1aca81ff47d 100644 --- a/examples/old/tls-record-layer/crypto/stale/Curve.Point.fst +++ b/examples/old/tls-record-layer/crypto/stale/Curve.Point.fst @@ -28,9 +28,7 @@ open Curve.Bigint open Curve.Bignum open FStar.UInt64 -module U8 = FStar.UInt8 module U32 = FStar.UInt32 -module U64 = FStar.UInt64 module U128 = FStar.UInt128 module HS = FStar.HyperStack diff --git a/examples/old/tls-record-layer/old/ulib/hyperstack/FStar.StackArray.fst b/examples/old/tls-record-layer/old/ulib/hyperstack/FStar.StackArray.fst index 3c8ec2cf77f..02f8f160920 100644 --- a/examples/old/tls-record-layer/old/ulib/hyperstack/FStar.StackArray.fst +++ b/examples/old/tls-record-layer/old/ulib/hyperstack/FStar.StackArray.fst @@ -22,7 +22,6 @@ open FStar.HyperStack open FStar.HST open FStar.UInt32 -module HH = FStar.HyperHeap module HS = FStar.HyperStack let u32 = UInt32.t diff --git a/examples/old/tls-record-layer/old/ulib/hyperstack/chacha.fst b/examples/old/tls-record-layer/old/ulib/hyperstack/chacha.fst index 19c9399d8b7..c5039e8e310 100644 --- a/examples/old/tls-record-layer/old/ulib/hyperstack/chacha.fst +++ b/examples/old/tls-record-layer/old/ulib/hyperstack/chacha.fst @@ -25,7 +25,6 @@ open FStar.UInt32 open FStar.Buffer module HH = FStar.HyperHeap -module HS = FStar.HyperStack let u32 = UInt32.t let u8 = UInt8.t diff --git a/examples/preorders/Closure.fst b/examples/preorders/Closure.fst index 3221d602471..134d7ca1ff6 100644 --- a/examples/preorders/Closure.fst +++ b/examples/preorders/Closure.fst @@ -17,7 +17,6 @@ module Closure open FStar.ReflexiveTransitiveClosure -module B = LowStar.Buffer module HS = FStar.HyperStack module HST = FStar.HyperStack.ST diff --git a/examples/preorders/NatHeap.fsti b/examples/preorders/NatHeap.fsti index d6b42f86f23..46a19ab2997 100644 --- a/examples/preorders/NatHeap.fsti +++ b/examples/preorders/NatHeap.fsti @@ -23,7 +23,6 @@ open FStar.Preorder (* NB: (a:Type0 & a) instead of dtuple2 is better notation *) -module F = FStar.FunctionalExtensionality //abstract val heap: Type u#1 diff --git a/examples/regional/RVector.fst b/examples/regional/RVector.fst index b0e8e484ece..17f3fca3303 100644 --- a/examples/regional/RVector.fst +++ b/examples/regional/RVector.fst @@ -7,7 +7,6 @@ open LowStar.Regional open LowStar.RVector open LowStar.Regional.Instances -module HS = FStar.HyperStack module HST = FStar.HyperStack.ST module HH = FStar.Monotonic.HyperHeap diff --git a/examples/rel/IfcMonitorTest.fst b/examples/rel/IfcMonitorTest.fst index 308c027c808..49b6a199f50 100644 --- a/examples/rel/IfcMonitorTest.fst +++ b/examples/rel/IfcMonitorTest.fst @@ -18,7 +18,6 @@ module IfcMonitorTest open Label open IfcMonitor open FStar.DM4F.Heap.IntStoreFixed -module T = FStar.Tactics assume val from_id (x:id) : GTot int assume diff --git a/examples/tactics/Imp.fst b/examples/tactics/Imp.fst index 8cd73ea198e..e88cb415c1a 100644 --- a/examples/tactics/Imp.fst +++ b/examples/tactics/Imp.fst @@ -36,7 +36,6 @@ type inst = //| Seq : prog -> inst and prog = list inst -module L = FStar.List.Tot let rec size : inst -> pos = function | Add _ _ _ diff --git a/examples/tactics/Printers.fst b/examples/tactics/Printers.fst index a5f1d99a09b..950f0660ed2 100644 --- a/examples/tactics/Printers.fst +++ b/examples/tactics/Printers.fst @@ -19,7 +19,6 @@ open FStar.List.Tot * much better now. *) open FStar.Tactics.V2 -module TD = FStar.Tactics.V2.Derived module TU = FStar.Tactics.Util let print_Prims_string : string -> Tot string = fun s -> "\"" ^ s ^ "\"" diff --git a/examples/tactics/old/StringPrinter.Rec.fst b/examples/tactics/old/StringPrinter.Rec.fst index e1e0f3b73c2..540df555b15 100644 --- a/examples/tactics/old/StringPrinter.Rec.fst +++ b/examples/tactics/old/StringPrinter.Rec.fst @@ -18,8 +18,6 @@ include StringPrinter.Base module T = FStar.Tactics.V2 -module Ca = FStar.Int.Cast -module U32 = FStar.UInt32 let tin_decr (a:Type) diff --git a/examples/typeclasses/Deriving.fst b/examples/typeclasses/Deriving.fst index 05c34f3f624..e7acce6e93f 100644 --- a/examples/typeclasses/Deriving.fst +++ b/examples/typeclasses/Deriving.fst @@ -5,7 +5,6 @@ open FStar.Class.Printable open FStar.List.Tot open FStar.Tactics.V2 -module TD = FStar.Tactics.V2.Derived module TU = FStar.Tactics.Util let mk_concat (sep : term) (ts : list term) : Tac term = diff --git a/src/basic/FStarC.Range.Type.fst b/src/basic/FStarC.Range.Type.fst index 911522308d7..132c689b7e0 100644 --- a/src/basic/FStarC.Range.Type.fst +++ b/src/basic/FStarC.Range.Type.fst @@ -20,7 +20,6 @@ open FStarC.Effect open FStarC.Class.Deq open FStarC.Class.Ord open FStarC.Order -module BU = FStarC.Util [@@ PpxDerivingYoJson; PpxDerivingShow ] type file_name = string diff --git a/tests/bug-reports/closed/Bug1750.Aux.fst b/tests/bug-reports/closed/Bug1750.Aux.fst index 0461e7bc83e..06ce513554e 100644 --- a/tests/bug-reports/closed/Bug1750.Aux.fst +++ b/tests/bug-reports/closed/Bug1750.Aux.fst @@ -1,9 +1,6 @@ module Bug1750.Aux -module HS = FStar.HyperStack -module HST = FStar.HyperStack.ST module MDM = FStar.Monotonic.DependentMap -module DM = FStar.DependentMap assume val pre_dhi :eqtype diff --git a/tests/bug-reports/closed/Bug2169.fst b/tests/bug-reports/closed/Bug2169.fst index 1bfd79e494c..00d83b86595 100644 --- a/tests/bug-reports/closed/Bug2169.fst +++ b/tests/bug-reports/closed/Bug2169.fst @@ -3,7 +3,6 @@ module Bug2169 open FStar.Tactics.V2 open FStar.List.Tot open FStar.FunctionalExtensionality -module T = FStar.Tactics.V2 open FStar.Monotonic.Pure diff --git a/tests/hacl/Lib.Exponentiation.Definition.fst b/tests/hacl/Lib.Exponentiation.Definition.fst index 70443d9659d..28930cc28c0 100644 --- a/tests/hacl/Lib.Exponentiation.Definition.fst +++ b/tests/hacl/Lib.Exponentiation.Definition.fst @@ -2,7 +2,6 @@ module Lib.Exponentiation.Definition open FStar.Mul -module Loops = Lib.LoopCombinators #set-options "--z3rlimit 50 --fuel 0 --ifuel 0" diff --git a/tests/hacl/Lib.Exponentiation.Definition.fsti b/tests/hacl/Lib.Exponentiation.Definition.fsti index 8b0359f418e..8951232f58a 100644 --- a/tests/hacl/Lib.Exponentiation.Definition.fsti +++ b/tests/hacl/Lib.Exponentiation.Definition.fsti @@ -2,7 +2,6 @@ module Lib.Exponentiation.Definition open FStar.Mul -module Loops = Lib.LoopCombinators #set-options "--z3rlimit 50 --fuel 0 --ifuel 0" diff --git a/tests/machine_integers/Test02.fst b/tests/machine_integers/Test02.fst index 44995d8f934..d9b362023c9 100644 --- a/tests/machine_integers/Test02.fst +++ b/tests/machine_integers/Test02.fst @@ -11,7 +11,6 @@ module U8 = FStar.UInt8 module U16 = FStar.UInt16 module U32 = FStar.UInt32 module U64 = FStar.UInt64 -module U128 = FStar.UInt128 let main () = (* This is awkward, but the branching makes this VC hard for Z3. The integer diff --git a/tests/machine_integers/TestChar.fst b/tests/machine_integers/TestChar.fst index 3caa3ecebe4..d872560ced0 100644 --- a/tests/machine_integers/TestChar.fst +++ b/tests/machine_integers/TestChar.fst @@ -4,7 +4,6 @@ open FStar.All open FStar.IO open FStar.Char -module U32 = FStar.UInt32 (* See issue #2131 *) let main () = diff --git a/tests/machine_integers/TestShift.fst b/tests/machine_integers/TestShift.fst index a1d4db1b2d3..0b93153a42f 100644 --- a/tests/machine_integers/TestShift.fst +++ b/tests/machine_integers/TestShift.fst @@ -7,15 +7,9 @@ open FStar.Int.Cast.Full open FStar.Tactics.V2 module I8 = FStar.Int8 -module I16 = FStar.Int16 module I32 = FStar.Int32 -module I64 = FStar.Int64 -module I128 = FStar.Int128 module U8 = FStar.UInt8 -module U16 = FStar.UInt16 module U32 = FStar.UInt32 -module U64 = FStar.UInt64 -module U128 = FStar.UInt128 let check s (b:bool) : ML unit = if not b then failwith s diff --git a/tests/micro-benchmarks/BinderAttributes.fst b/tests/micro-benchmarks/BinderAttributes.fst index 8427c410e6e..3fda052e7e3 100644 --- a/tests/micro-benchmarks/BinderAttributes.fst +++ b/tests/micro-benchmarks/BinderAttributes.fst @@ -1,7 +1,6 @@ module BinderAttributes module T = FStar.Tactics.V2 -module R = FStar.Reflection.V2 open FStar.List.Tot let default_to (def : 'a) (x : option 'a) : Tot 'a = diff --git a/tests/micro-benchmarks/BoxBitVec.fst b/tests/micro-benchmarks/BoxBitVec.fst index 0d15f38c7de..e6d2952bd65 100644 --- a/tests/micro-benchmarks/BoxBitVec.fst +++ b/tests/micro-benchmarks/BoxBitVec.fst @@ -1,5 +1,4 @@ module BoxBitVec -module U = FStar.UInt module BV = FStar.BV open FStar.BV let test (x:BV.bv_t 3) = BV.bvdiv x 1 diff --git a/tests/micro-benchmarks/BvBinaryOps.fst b/tests/micro-benchmarks/BvBinaryOps.fst index 7922aca5199..cd6087d0906 100644 --- a/tests/micro-benchmarks/BvBinaryOps.fst +++ b/tests/micro-benchmarks/BvBinaryOps.fst @@ -1,9 +1,7 @@ module BvBinaryOps module BV = FStar.BV -module BitVector = FStar.BitVector -module Tac = FStar.Tactics module UInt = FStar.UInt diff --git a/tests/micro-benchmarks/NormPureSubtermsWithinComputations.fst b/tests/micro-benchmarks/NormPureSubtermsWithinComputations.fst index 39e54710887..7e9e91e80d4 100644 --- a/tests/micro-benchmarks/NormPureSubtermsWithinComputations.fst +++ b/tests/micro-benchmarks/NormPureSubtermsWithinComputations.fst @@ -1,7 +1,6 @@ module NormPureSubtermsWithinComputations open FStar.HyperStack.All open FStar.HyperStack -module ST = FStar.HyperStack.ST open FStar.List.Tot open FStar.Tactics.V2 diff --git a/tests/micro-benchmarks/Test.Delta.Namespace.fst b/tests/micro-benchmarks/Test.Delta.Namespace.fst index 0dfe96345cb..853cad82e02 100644 --- a/tests/micro-benchmarks/Test.Delta.Namespace.fst +++ b/tests/micro-benchmarks/Test.Delta.Namespace.fst @@ -1,7 +1,6 @@ module Test.Delta.Namespace module L = FStar.List.Tot open FStar.Tactics.V2 -module P = FStar.Printf let f (x:int) = x + 1 let m (y:list int) = L.map f y diff --git a/tests/micro-benchmarks/TestWellFoundedRecursion.fst b/tests/micro-benchmarks/TestWellFoundedRecursion.fst index b6b022a521c..8c452b4a9cb 100644 --- a/tests/micro-benchmarks/TestWellFoundedRecursion.fst +++ b/tests/micro-benchmarks/TestWellFoundedRecursion.fst @@ -114,7 +114,6 @@ let rec map_test2 (#a #b:Type) (t:test2 a) (f: a -> b) : test2 b = Test2 (Test1 (fun (x:nat) -> wf_test1 (Test1 g) x; map_test2 #a #b (g x) f)) ////////////////////////////////////////////////////////////////////////////////////////// -module F = FStar.FunctionalExtensionality open FStar.FunctionalExtensionality noeq type tf = diff --git a/tests/micro-benchmarks/TwoPhaseTC.fst b/tests/micro-benchmarks/TwoPhaseTC.fst index 95ac45959bc..7824f1a630d 100644 --- a/tests/micro-benchmarks/TwoPhaseTC.fst +++ b/tests/micro-benchmarks/TwoPhaseTC.fst @@ -18,7 +18,6 @@ module TwoPhaseTC #set-options "--ugly" open FStar.Classical -module PropExt = FStar.PropositionalExtensionality #set-options "--max_fuel 0 --max_ifuel 0 --initial_fuel 0 --initial_ifuel 0" diff --git a/tests/struct/taggedunion.pos/Test.fst b/tests/struct/taggedunion.pos/Test.fst index ce977acf661..9168d7e91c7 100644 --- a/tests/struct/taggedunion.pos/Test.fst +++ b/tests/struct/taggedunion.pos/Test.fst @@ -16,7 +16,6 @@ module Test module TU = FStar.TaggedUnion -module HS = FStar.HyperStack module HST = FStar.HyperStack.ST module P = FStar.Pointer diff --git a/tests/vale/X64.Vale.StateLemmas_i.fst b/tests/vale/X64.Vale.StateLemmas_i.fst index 1ab74dbc5e7..5735f16faf5 100644 --- a/tests/vale/X64.Vale.StateLemmas_i.fst +++ b/tests/vale/X64.Vale.StateLemmas_i.fst @@ -18,7 +18,6 @@ open X64.Machine_s open X64.Vale.State_i open FStar.UInt module S = X64.Semantics_s -module M = TransparentMap module F = FStar.FunctionalExtensionality diff --git a/tests/vale/X64.Vale.StateLemmas_i.fsti b/tests/vale/X64.Vale.StateLemmas_i.fsti index 13297e6fa3e..ff668b7e9d2 100644 --- a/tests/vale/X64.Vale.StateLemmas_i.fsti +++ b/tests/vale/X64.Vale.StateLemmas_i.fsti @@ -19,7 +19,6 @@ open X64.Vale.State_i open FStar.UInt open FStar.FunctionalExtensionality module S = X64.Semantics_s -module M = TransparentMap unfold let ok' = S.Mkstate?.ok unfold let regs' = S.Mkstate?.regs diff --git a/ulib/FStar.Bytes.fsti b/ulib/FStar.Bytes.fsti index 5092aa1e02e..451566b805e 100644 --- a/ulib/FStar.Bytes.fsti +++ b/ulib/FStar.Bytes.fsti @@ -29,13 +29,10 @@ bytes, and with support for machine integers and C-extractible versions module FStar.Bytes module S = FStar.Seq -module U = FStar.UInt module U8 = FStar.UInt8 module U16 = FStar.UInt16 module U32 = FStar.UInt32 -module U64 = FStar.UInt64 module Str = FStar.String -module Chr = FStar.Char unfold let u8 = U8.t unfold let u16 = U16.t diff --git a/ulib/FStar.FiniteMap.Base.fsti b/ulib/FStar.FiniteMap.Base.fsti index 0c4d69c4a1b..d19d54d0c5c 100644 --- a/ulib/FStar.FiniteMap.Base.fsti +++ b/ulib/FStar.FiniteMap.Base.fsti @@ -37,7 +37,6 @@ finite maps as they're modeled in Dafny. module FStar.FiniteMap.Base open FStar.FunctionalExtensionality -module FLT = FStar.List.Tot module FSet = FStar.FiniteSet.Base type setfun_t (a: eqtype) diff --git a/ulib/FStar.Matrix.fst b/ulib/FStar.Matrix.fst index bca2a15b210..0109c4fcf2e 100644 --- a/ulib/FStar.Matrix.fst +++ b/ulib/FStar.Matrix.fst @@ -30,7 +30,6 @@ module CF = FStar.Algebra.CommMonoid.Fold module SP = FStar.Seq.Permutation module SB = FStar.Seq.Base module SProp = FStar.Seq.Properties -module ML = FStar.Math.Lemmas open FStar.IntegerIntervals open FStar.Mul diff --git a/ulib/FStar.Modifies.fst b/ulib/FStar.Modifies.fst index 106a2910789..91661ac6a13 100644 --- a/ulib/FStar.Modifies.fst +++ b/ulib/FStar.Modifies.fst @@ -16,9 +16,7 @@ module FStar.Modifies module HS = FStar.HyperStack -module HST = FStar.HyperStack.ST module B = FStar.Buffer -module U32 = FStar.UInt32 noeq type loc_aux : Type = diff --git a/ulib/FStar.ModifiesGen.fst b/ulib/FStar.ModifiesGen.fst index 6f4f459bb53..87c450917bf 100644 --- a/ulib/FStar.ModifiesGen.fst +++ b/ulib/FStar.ModifiesGen.fst @@ -18,7 +18,6 @@ module FStar.ModifiesGen #set-options "--split_queries no" module HS = FStar.HyperStack -module HST = FStar.HyperStack.ST noeq type aloc (#al: aloc_t) (c: cls al) = | ALoc: diff --git a/ulib/FStar.Monotonic.DependentMap.fst b/ulib/FStar.Monotonic.DependentMap.fst index 5ad55dcc133..1422920090e 100644 --- a/ulib/FStar.Monotonic.DependentMap.fst +++ b/ulib/FStar.Monotonic.DependentMap.fst @@ -18,7 +18,6 @@ module FStar.Monotonic.DependentMap that grow monotonically, while subject to an invariant on the entire map *) open FStar.HyperStack.ST -module HS = FStar.HyperStack module DM = FStar.DependentMap /// `map a b`: Represent the partial map as a list of pairs of points diff --git a/ulib/FStar.Monotonic.HyperHeap.fst b/ulib/FStar.Monotonic.HyperHeap.fst index 284ef0cf097..c74f1307c0f 100644 --- a/ulib/FStar.Monotonic.HyperHeap.fst +++ b/ulib/FStar.Monotonic.HyperHeap.fst @@ -15,8 +15,6 @@ *) module FStar.Monotonic.HyperHeap -module Set = FStar.Set -module Map = FStar.Map open FStar.Monotonic.Heap open FStar.Ghost diff --git a/ulib/FStar.Printf.fst b/ulib/FStar.Printf.fst index 6c647d8a79d..a9eae6cd652 100644 --- a/ulib/FStar.Printf.fst +++ b/ulib/FStar.Printf.fst @@ -22,7 +22,6 @@ module FStar.Printf open FStar.Char open FStar.String -module I = FStar.Integers noeq type extension = diff --git a/ulib/FStar.Reflection.TermEq.fsti b/ulib/FStar.Reflection.TermEq.fsti index f8856cbff68..11f292eb793 100644 --- a/ulib/FStar.Reflection.TermEq.fsti +++ b/ulib/FStar.Reflection.TermEq.fsti @@ -3,7 +3,6 @@ module FStar.Reflection.TermEq open FStar.Stubs.Reflection.Types open FStar.Stubs.Reflection.V2.Data open FStar.Stubs.Reflection.V2.Builtins -module L = FStar.List.Tot (* Auxiliary... would be good to move. *) let rec allP0 #a (pred : a -> Type0) (l : list a) : Type0 = diff --git a/ulib/FStar.SizeT.fst b/ulib/FStar.SizeT.fst index dbfb19c327b..22964e37f60 100644 --- a/ulib/FStar.SizeT.fst +++ b/ulib/FStar.SizeT.fst @@ -1,6 +1,5 @@ module FStar.SizeT open FStar.Ghost -module I64 = FStar.Int64 (* This is only intended as a model, but will be extracted natively by Krml with the correct C semantics *) diff --git a/ulib/FStar.TSet.fst b/ulib/FStar.TSet.fst index e84f7246884..8c4f3c15ea9 100644 --- a/ulib/FStar.TSet.fst +++ b/ulib/FStar.TSet.fst @@ -18,7 +18,6 @@ module FStar.TSet #set-options "--initial_fuel 0 --max_fuel 0 --initial_ifuel 0 --max_ifuel 0" -module P = FStar.PropositionalExtensionality module F = FStar.FunctionalExtensionality (* diff --git a/ulib/FStar.Tactics.V1.Derived.fst b/ulib/FStar.Tactics.V1.Derived.fst index a4478fa47b2..55e67ad80d4 100644 --- a/ulib/FStar.Tactics.V1.Derived.fst +++ b/ulib/FStar.Tactics.V1.Derived.fst @@ -27,7 +27,6 @@ open FStar.Stubs.VConfig include FStar.Tactics.Names module L = FStar.List.Tot.Base -module V = FStar.Tactics.Visit private let (@) = L.op_At let name_of_bv (bv : bv) : Tac string = diff --git a/ulib/FStar.Tactics.V2.Derived.fst b/ulib/FStar.Tactics.V2.Derived.fst index 5dd819eae9e..a9d47a73e11 100644 --- a/ulib/FStar.Tactics.V2.Derived.fst +++ b/ulib/FStar.Tactics.V2.Derived.fst @@ -29,7 +29,6 @@ open FStar.Tactics.V2.SyntaxCoercions include FStar.Tactics.Names module L = FStar.List.Tot.Base -module V = FStar.Tactics.Visit private let (@) = L.op_At private diff --git a/ulib/FStar.Vector.Properties.fst b/ulib/FStar.Vector.Properties.fst index 6c46296e9d7..24765566bb6 100644 --- a/ulib/FStar.Vector.Properties.fst +++ b/ulib/FStar.Vector.Properties.fst @@ -16,7 +16,6 @@ module FStar.Vector.Properties open FStar.Vector.Base -module S = FStar.Seq module U32 = FStar.UInt32 /// This coercion seems to be necessary in some places diff --git a/ulib/LowStar.Buffer.fst b/ulib/LowStar.Buffer.fst index 75d9b69432d..7c30018d59f 100644 --- a/ulib/LowStar.Buffer.fst +++ b/ulib/LowStar.Buffer.fst @@ -17,12 +17,8 @@ module LowStar.Buffer include LowStar.Monotonic.Buffer -module P = FStar.Preorder -module G = FStar.Ghost -module U32 = FStar.UInt32 module Seq = FStar.Seq -module HS = FStar.HyperStack module HST = FStar.HyperStack.ST (* diff --git a/ulib/LowStar.BufferOps.fst b/ulib/LowStar.BufferOps.fst index a0f478e58a2..28a9ac76c7e 100644 --- a/ulib/LowStar.BufferOps.fst +++ b/ulib/LowStar.BufferOps.fst @@ -20,13 +20,9 @@ module LowStar.BufferOps and notations into the scope without bringing any definition from LowStar.Buffer into the scope. *) -module HS = FStar.HyperStack module HST = FStar.HyperStack.ST -module U32 = FStar.UInt32 -module G = FStar.Ghost module Seq = FStar.Seq module B = LowStar.Buffer -module L = FStar.List.Tot inline_for_extraction unfold diff --git a/ulib/LowStar.BufferView.Up.fsti b/ulib/LowStar.BufferView.Up.fsti index 113983a3614..0ae60481cd9 100644 --- a/ulib/LowStar.BufferView.Up.fsti +++ b/ulib/LowStar.BufferView.Up.fsti @@ -31,7 +31,6 @@ module LowStar.BufferView.Up open LowStar.Monotonic.Buffer module HS=FStar.HyperStack -module B=LowStar.Monotonic.Buffer module Down=LowStar.BufferView.Down (** Definition of a view **) diff --git a/ulib/LowStar.ConstBuffer.fst b/ulib/LowStar.ConstBuffer.fst index 1359d632b67..66636c42a3f 100644 --- a/ulib/LowStar.ConstBuffer.fst +++ b/ulib/LowStar.ConstBuffer.fst @@ -15,13 +15,9 @@ *) module LowStar.ConstBuffer -module U32 = FStar.UInt32 -module Seq = FStar.Seq -module HS = FStar.HyperStack open FStar.HyperStack.ST -module I = LowStar.ImmutableBuffer module B = LowStar.Buffer let const_buffer a = qbuf a diff --git a/ulib/LowStar.ImmutableBuffer.fst b/ulib/LowStar.ImmutableBuffer.fst index 564c00f2506..f04e9c739a6 100644 --- a/ulib/LowStar.ImmutableBuffer.fst +++ b/ulib/LowStar.ImmutableBuffer.fst @@ -17,7 +17,6 @@ module LowStar.ImmutableBuffer include LowStar.Monotonic.Buffer -module P = FStar.Preorder module G = FStar.Ghost module U32 = FStar.UInt32 module Seq = FStar.Seq diff --git a/ulib/LowStar.PrefixFreezableBuffer.fst b/ulib/LowStar.PrefixFreezableBuffer.fst index d6f618db11b..d03a401dafc 100644 --- a/ulib/LowStar.PrefixFreezableBuffer.fst +++ b/ulib/LowStar.PrefixFreezableBuffer.fst @@ -20,14 +20,10 @@ open FStar.HyperStack.ST include LowStar.Monotonic.Buffer -module P = FStar.Preorder -module G = FStar.Ghost -module U8 = FStar.UInt8 module U32 = FStar.UInt32 module Seq = FStar.Seq -module HS = FStar.HyperStack module ST = FStar.HyperStack.ST module E = FStar.Endianness diff --git a/ulib/LowStar.PrefixFreezableBuffer.fsti b/ulib/LowStar.PrefixFreezableBuffer.fsti index 46ec82badc1..265c702c049 100644 --- a/ulib/LowStar.PrefixFreezableBuffer.fsti +++ b/ulib/LowStar.PrefixFreezableBuffer.fsti @@ -20,14 +20,12 @@ open FStar.HyperStack.ST include LowStar.Monotonic.Buffer -module P = FStar.Preorder module G = FStar.Ghost module U32 = FStar.UInt32 module Seq = FStar.Seq module HS = FStar.HyperStack -module ST = FStar.HyperStack.ST (* * A library for prefix freezable buffers of elements of type u8 diff --git a/ulib/LowStar.UninitializedBuffer.fst b/ulib/LowStar.UninitializedBuffer.fst index e6082579d97..83ad7780c57 100644 --- a/ulib/LowStar.UninitializedBuffer.fst +++ b/ulib/LowStar.UninitializedBuffer.fst @@ -17,8 +17,6 @@ module LowStar.UninitializedBuffer include LowStar.Monotonic.Buffer -module P = FStar.Preorder -module G = FStar.Ghost module U32 = FStar.UInt32 module Seq = FStar.Seq diff --git a/ulib/legacy/FStar.Buffer.fst b/ulib/legacy/FStar.Buffer.fst index 1bf7092d5db..406937f5a69 100644 --- a/ulib/legacy/FStar.Buffer.fst +++ b/ulib/legacy/FStar.Buffer.fst @@ -17,7 +17,6 @@ module FStar.Buffer open FStar.Seq open FStar.UInt32 -module Int32 = FStar.Int32 open FStar.HyperStack open FStar.HyperStack.ST open FStar.Ghost diff --git a/ulib/legacy/FStar.Pointer.Derived1.fst b/ulib/legacy/FStar.Pointer.Derived1.fst index 13ac7cd0f20..07732ed3e77 100644 --- a/ulib/legacy/FStar.Pointer.Derived1.fst +++ b/ulib/legacy/FStar.Pointer.Derived1.fst @@ -15,8 +15,6 @@ *) module FStar.Pointer.Derived1 -module HH = FStar.HyperStack -module HS = FStar.HyperStack module HST = FStar.HyperStack.ST let includes_gfield_gen #t p #l q fd = diff --git a/ulib/legacy/FStar.Pointer.Derived2.fst b/ulib/legacy/FStar.Pointer.Derived2.fst index f8df5b6c23f..d3920406b11 100644 --- a/ulib/legacy/FStar.Pointer.Derived2.fst +++ b/ulib/legacy/FStar.Pointer.Derived2.fst @@ -15,7 +15,6 @@ *) module FStar.Pointer.Derived2 -module HH = FStar.HyperStack module HS = FStar.HyperStack module HST = FStar.HyperStack.ST diff --git a/ulib/legacy/FStar.Pointer.Derived2.fsti b/ulib/legacy/FStar.Pointer.Derived2.fsti index d5b3a4b6f46..55add405cc3 100644 --- a/ulib/legacy/FStar.Pointer.Derived2.fsti +++ b/ulib/legacy/FStar.Pointer.Derived2.fsti @@ -17,7 +17,6 @@ module FStar.Pointer.Derived2 include FStar.Pointer.Base include FStar.Pointer.Derived1 -module HH = FStar.HyperStack module HS = FStar.HyperStack module HST = FStar.HyperStack.ST diff --git a/ulib/legacy/FStar.Pointer.Derived3.fst b/ulib/legacy/FStar.Pointer.Derived3.fst index 60d00c692a5..f30e0fb46ca 100644 --- a/ulib/legacy/FStar.Pointer.Derived3.fst +++ b/ulib/legacy/FStar.Pointer.Derived3.fst @@ -15,7 +15,6 @@ *) module FStar.Pointer.Derived3 -module HH = FStar.HyperStack module HS = FStar.HyperStack module HST = FStar.HyperStack.ST diff --git a/ulib/legacy/FStar.Pointer.Derived3.fsti b/ulib/legacy/FStar.Pointer.Derived3.fsti index 408c4ac1d4a..71a305b9085 100644 --- a/ulib/legacy/FStar.Pointer.Derived3.fsti +++ b/ulib/legacy/FStar.Pointer.Derived3.fsti @@ -18,7 +18,6 @@ include FStar.Pointer.Base include FStar.Pointer.Derived1 // include FStar.Pointer.Derived2 // useless here -module HH = FStar.HyperStack module HS = FStar.HyperStack module HST = FStar.HyperStack.ST diff --git a/ulib/legacy/LowStar.BufferCompat.fst b/ulib/legacy/LowStar.BufferCompat.fst index 6a037223b83..f985f525eb5 100644 --- a/ulib/legacy/LowStar.BufferCompat.fst +++ b/ulib/legacy/LowStar.BufferCompat.fst @@ -19,7 +19,6 @@ include LowStar.Buffer module HS = FStar.HyperStack module HST = FStar.HyperStack.ST module U32 = FStar.UInt32 -module G = FStar.Ghost module Seq = FStar.Seq unfold diff --git a/ulib/ml/app/FStar_Bytes.ml b/ulib/ml/app/FStar_Bytes.ml index ac80dca1b1b..33a3b2a591c 100644 --- a/ulib/ml/app/FStar_Bytes.ml +++ b/ulib/ml/app/FStar_Bytes.ml @@ -1,7 +1,6 @@ module U8 = FStar_UInt8 module U16 = FStar_UInt16 module U32 = FStar_UInt32 -module U64 = FStar_UInt64 type u8 = U8.t type u16 = U16.t diff --git a/ulib/ml/plugin/FStarC_Tactics_V1_Builtins.ml b/ulib/ml/plugin/FStarC_Tactics_V1_Builtins.ml index ef0bc1b2ca7..8726a636de8 100644 --- a/ulib/ml/plugin/FStarC_Tactics_V1_Builtins.ml +++ b/ulib/ml/plugin/FStarC_Tactics_V1_Builtins.ml @@ -5,14 +5,9 @@ open FStar_Pervasives open FStarC_Tactics_Result open FStarC_Tactics_Types -module N = FStarC_TypeChecker_Normalize module B = FStarC_Tactics_V1_Basic module TM = FStarC_Tactics_Monad module CTRW = FStarC_Tactics_CtrlRewrite -module RD = FStarC_Reflection_V1_Data -module EMB = FStarC_Syntax_Embeddings -module EMBBase = FStarC_Syntax_Embeddings_Base -module NBET = FStarC_TypeChecker_NBETerm type ('a,'wp) tac_repr = proofstate -> 'a __result type 'a __tac = ('a, unit) tac_repr diff --git a/ulib/ml/plugin/FStarC_Tactics_V2_Builtins.ml b/ulib/ml/plugin/FStarC_Tactics_V2_Builtins.ml index f47e475f23a..5eba4694aa7 100644 --- a/ulib/ml/plugin/FStarC_Tactics_V2_Builtins.ml +++ b/ulib/ml/plugin/FStarC_Tactics_V2_Builtins.ml @@ -5,15 +5,9 @@ open FStar_Pervasives open FStarC_Tactics_Result open FStarC_Tactics_Types -module N = FStarC_TypeChecker_Normalize module B = FStarC_Tactics_V2_Basic module TM = FStarC_Tactics_Monad module CTRW = FStarC_Tactics_CtrlRewrite -module RT = FStarC_Reflection_Types -module RD = FStarC_Reflection_V1_Data -module EMB = FStarC_Syntax_Embeddings -module EMBBase = FStarC_Syntax_Embeddings_Base -module NBET = FStarC_TypeChecker_NBETerm type ('a,'wp) tac_repr = proofstate -> 'a __result type 'a __tac = ('a, unit) tac_repr