Documenting the library

The table below lists all files in ulib together with an a documentation owner.

Please sign up to own files that are not yet assigned.

Documentation work takes place in the shared fstardoc branch.

Please look files that are marked "done" for documentation style. Briefly:

• Include a top-level description of the intent of the module in a /// comment

• Add a (** *) comment to every top-level definition

• In both kinds of comments, inline code fragments are delimited with a []

• For multi-line code blocks, use {[ ]} delimiters

• Focus primarily on documenting what's there. If you see opportunities for code improvement, please note them in TODOs, unless those improvements are trivially applicable.

• Prioritize documenting interface files, i.e., .fsti

• Once you're done adding documentation, you should

  • Add your file to the DOC_FILES variable at the end of ulib/Makefile

  • run make fstardoc, which will format your file using fstar --print_in_place and run fstardoc.py to extract a .md file from it.

    • Note, this will reformat your file to conform to formatting guidelines.

    • Note, --print_in_place does not yet enforce any whitespace conventions, notably in comments. We will enhance it to remove all trailing whitespace.

  • We will eventually run make fstardoc as part of CI and complain if a file in ulib changes when reformatted.

  • Note, fstardoc.py still has some limitations in the formatting. We will work simultaneously on improving its output

  • For now, the generated .md files are not yet hosted anywhere. You can optionally upload them manually to the fstardoc branch of fstarlang.github.io, if you wish. We will eventually automate this process in CI.

Table of modules

Assigned to	File name	Notes
nik	prims.fst	done; core
nik	FStar.Pervasives.fst	done; core
nik	FStar.Pervasives.Native.fst	done; core
nik	FStar.Squash.fsti	done; core
nik	FStar.Squash.fst	core
nik/denis/jay	FStar.Classical.fsti	done; core
nik/denis/jay	FStar.Classical.fst	core
	FStar.Algebra.CommMonoid.fst	math
	FStar.Algebra.Monoid.fst	math
nik	FStar.All.fst	effects
	FStar.Array.fst	Superceded by LowStar.Buffer?
	FStar.Array.fsti	idem
	FStar.Axiomatic.Array.fst	idem
nik	FStar.BaseTypes.fsti	done; core
nik	FStar.BigOps.fst	core
nik	FStar.BigOps.fsti	done; core
nik	FStar.BitVector.fst	done; core
	FStar.Buffer.fst
	FStar.Buffer.Quantifiers.fst
	FStar.BufferNG.fst
nik	FStar.BV.fst	core
nik	FStar.BV.fsti	done;core
	FStar.Bytes.fsti
	FStar.Calc.fst	core
nik	FStar.Char.fsti	done
nik	FStar.ConstantTime.Integers.fst	experimental
nik	FStar.ConstantTime.Integers.fsti	done; experimental
	FStar.Constructive.fst	legacy
	FStar.Crypto.fst
nik	FStar.Date.fsti	done; native
nik	FStar.DependentMap.fsti	done; container
nik	FStar.DependentMap.fst	container
nik	FStar.Dyn.fsti	done; native
	FStar.Endianness.fst	core
	FStar.Endianness.fsti	core
	FStar.ErasedLogic.fst	legacy
	FStar.Error.fst	superceded by Prims.either
nik	FStar.Exn.fst	done; native
nik	FStar.Fin.fst	done; math
nik	FStar.Float.fsti	done; native
nik	FStar.FunctionalExtensionality.fst	core
nik	FStar.FunctionalExtensionality.fsti	done; core
nik	FStar.Ghost.fsti	done; core
nik	FStar.Ghost.fst	core
aseem	FStar.GSet.fst	container
aseem	FStar.GSet.fsti	container
aseem	FStar.Heap.fst	memory-model
aseem	FStar.HyperStack.All.fst	effect
aseem	FStar.HyperStack.fst	memory-model
	FStar.HyperStack.IO.fst	merge with FStar.Effect.HyperStack.ML?
aseem	FStar.HyperStack.ST.fst	effect
aseem	FStar.HyperStack.ST.fsti	effect
nik	FStar.IFC.fst	done;
nik	FStar.IndefiniteDescription.fst	done; core
	FStar.Int.Cast.fst	numeric
	FStar.Int.Cast.Full.fst	numeric (merge with FStar.Int.Cast)?
	FStar.Int.fst	numeric
	FStar.Int128.fst	numeric
	FStar.Int16.fst	numeric
	FStar.Int31.fst	numeric
	FStar.Int32.fst	numeric
	FStar.Int63.fst	numeric
	FStar.Int64.fst	numeric
	FStar.Int8.fst	numeric
	FStar.Integers.fst	numeric
nik	FStar.IO.fst	core
nik	FStar.List.fst	container
nik	FStar.List.Pure.Base.fst	container
nik	FStar.List.Pure.fst	container
nik	FStar.List.Pure.Properties.fst	container
nik	FStar.List.Tot.Base.fst	container
nik	FStar.List.Tot.fst	container
nik	FStar.List.Tot.Properties.fst	container
aseem	FStar.Map.fst	container
aseem	FStar.Map.fsti	container
	FStar.MarkovsPrinciple.fst	math
aymeric	FStar.Math.Lemmas.fst	math
	FStar.Math.Lib.fst	math
	FStar.Matrix2.fsti	container
	FStar.Modifies.fst	memory-model
	FStar.Modifies.fsti	memory-model
	FStar.ModifiesGen.fst	memory-model
	FStar.ModifiesGen.fsti	memory-model
	FStar.Monotonic.DependentMap.fst	container
	FStar.Monotonic.DependentMap.fsti	container
aseem	FStar.Monotonic.Heap.fst	memory-model
aseem	FStar.Monotonic.Heap.fsti	memory-model
aseem	FStar.Monotonic.HyperHeap.fst	memory-model
aseem	FStar.Monotonic.HyperHeap.fsti	memory-model
aseem	FStar.Monotonic.HyperStack.fst	memory-model
aseem	FStar.Monotonic.HyperStack.fsti	memory-model
aseem	FStar.Monotonic.Map.fst	container
aseem	FStar.Monotonic.Seq.fst	container
aseem	FStar.Monotonic.Witnessed.fst	memory-model
aseem	FStar.Monotonic.Witnessed.fsti	memory-model
aseem	FStar.MRef.fst	memory-model
nik	FStar.Mul.fst	core
nik	FStar.Option.fst	core
aseem	FStar.Order.fst	math
aseem	FStar.OrdMap.fst	container
aseem	FStar.OrdMapProps.fst	container
aseem	FStar.OrdSet.fst	container
aseem	FStar.OrdSetProps.fst	container
	FStar.Pointer.Base.fst	memory-model
	FStar.Pointer.Base.fsti	memory-model
	FStar.Pointer.Derived1.fst	memory-model
	FStar.Pointer.Derived1.fsti	memory-model
	FStar.Pointer.Derived2.fst	memory-model
	FStar.Pointer.Derived2.fsti	memory-model
	FStar.Pointer.Derived3.fst	memory-model
	FStar.Pointer.Derived3.fsti	memory-model
	FStar.Pointer.fst	memory-model
nik	FStar.PredicateExtensionality.fst	core
aseem	FStar.Preorder.fst	math
nik	FStar.Printf.fst	core
nik	FStar.PropositionalExtensionality.fst	core
nik	FStar.Range.fsti	native
nik	FStar.Reader.fst	effect
nik	FStar.Real.fsti	numeric
aseem	FStar.Ref.fst	memory-model
	FStar.Reflection.Arith.fst	reflection
	FStar.Reflection.Basic.fst	reflection
	FStar.Reflection.Const.fst	reflection
	FStar.Reflection.Data.fst	reflection
	FStar.Reflection.Derived.fst	reflection
	FStar.Reflection.Derived.Lemmas.fst	reflection
	FStar.Reflection.Formula.fst	reflection
	FStar.Reflection.fst	reflection
	FStar.Reflection.Types.fsti	reflection
santiago	FStar.ReflexiveTransitiveClosure.fst	math
santiago	FStar.ReflexiveTransitiveClosure.fsti	math
	FStar.Relational.Comp.fst	legacy
	FStar.Relational.Relational.fst	legacy
	FStar.Relational.State.fst	legacy
nik	FStar.Seq.Base.fst	container
nik	FStar.Seq.fst	container
nik	FStar.Seq.Properties.fst	container
nik	FStar.Seq.Sorted.fst	container
aseem	FStar.Set.fst	container
aseem	FStar.Set.fsti	container
aseem	FStar.SquashProperties.fst	core
aseem	FStar.ST.fst	effect
nik	FStar.String.fsti	native
nik	FStar.StrongExcludedMiddle.fst	core
	FStar.Tactics.Arith.fst	tactics
	FStar.Tactics.Builtins.fst	tactics
	FStar.Tactics.BV.fst	tactics
	FStar.Tactics.Canon.fst	tactics
	FStar.Tactics.CanonCommMonoid.fst	tactics
	FStar.Tactics.CanonCommMonoidSimple.fst	tactics
santiago	FStar.Tactics.CanonCommSemiring.fst	tactics
	FStar.Tactics.CanonCommSwaps.fst	tactics
	FStar.Tactics.CanonMonoid.fst	tactics
	FStar.Tactics.Derived.fst	tactics
	FStar.Tactics.Effect.fst	tactics
	FStar.Tactics.fst	tactics
	FStar.Tactics.Logic.fst	tactics
	FStar.Tactics.PatternMatching.fst	tactics
	FStar.Tactics.Result.fst	tactics
	FStar.Tactics.Simplifier.fst	tactics
	FStar.Tactics.Typeclasses.fst	tactics
	FStar.Tactics.Types.fsti	tactics
	FStar.Tactics.Util.fst	tactics
	FStar.TaggedUnion.fst
	FStar.TaggedUnion.fsti
	FStar.Tcp.fsti	native
aseem	FStar.TSet.fst	container
	FStar.TwoLevelHeap.fst	memory-model; deprecate
	FStar.Udp.fsti	container
	FStar.UInt.fst	numeric
	FStar.UInt128.fst	numeric
	FStar.UInt128.fsti	numeric
nik	FStar.UInt16.fst	done;numeric
	FStar.UInt31.fst	numeric
nik	FStar.UInt32.fst	done;numeric
	FStar.UInt63.fst	numeric
nik	FStar.UInt64.fst	done;numeric
nik	FStar.UInt8.fst	done;numeric
aseem	FStar.Universe.fst	core
aseem	FStar.Universe.fsti	core
	FStar.Util.fst	core (defunct?)
	FStar.Vector.Base.fst	container
	FStar.Vector.Base.fsti	container
	FStar.Vector.fst	container
	FStar.Vector.Properties.fst	container
nik	FStar.WellFounded.fst	math
	LowStar.Buffer.fst	container
	LowStar.BufferCompat.fst
	LowStar.BufferOps.fst	container
nik	LowStar.BufferView.Down.fst	container
nik	LowStar.BufferView.Down.fsti	container
nik	LowStar.BufferView.fst	container
nik	LowStar.BufferView.fsti	container
nik	LowStar.BufferView.Up.fst	container
nik	LowStar.BufferView.Up.fsti	container
nik	LowStar.ConstBuffer.fst	container
nik	LowStar.ConstBuffer.fsti	container
	LowStar.Endianness.fst	core
	LowStar.ImmutableBuffer.fst	container
	LowStar.Literal.fsti	core
	LowStar.Modifies.fst	memory-model
	LowStar.ModifiesPat.fst	memory-model
	LowStar.Monotonic.Buffer.fst	container
	LowStar.Monotonic.Buffer.fsti	container
	LowStar.PrefixFreezableBuffer.fst	container
	LowStar.PrefixFreezableBuffer.fsti	container
nik	LowStar.Printf.fst	core
	LowStar.Regional.fst	memory-model
	LowStar.Regional.Instances.fst	memory-model
	LowStar.RVector.fst	container
	LowStar.ToFStarBuffer.fst
	LowStar.UninitializedBuffer.fst	container
	LowStar.Vector.fst	container
denis	Steel.Memory.fsti	steel; memory-model
denis	Steel.Memory.fst	steel; memory-model
denis	Steel.Actions.fsti	steel; memory-model
denis	Steel.Actions.fst	steel; memory-model
nik/aseem	Steel.Semantics.Hoare.MST.fst	steel; semantics
nik/aseem	Steel.Actions.fst	steel; memory-model
aseem	Steel.Semantics.Instantiate.fsti	steel; semantics
aseem	Steel.Semantics.Instantiate.fst	steel; semantics
aymeric	Steel.Memory.Tactics.fst	steel
nik	Steel.Channel.Protocol.fst	steel
nik	Steel.Channel.Simplex.fst	steel
nik	Steel.Channel.Simplex.fsti	steel
aymeric	Steel.Effect.Atomic.fst	steel
aseem	Steel.Effect.fst	steel
denis/aymeric	Steel.HigherReference.fst	steel
denis/aymeric	Steel.HigherReference.fsti	steel
denis/aymeric	Steel.Reference.fst	steel
denis/aymeric	Steel.Reference.fsti	steel
nik	Steel.PCM.fst	steel
nik	Steel.PCM.Memory.fsti	steel
nik	Steel.PCM.Memory.fst	steel
nik	Steel.Primitive.ForkJoin.fst	steel
nik	Steel.Primitive.ForkJoin.fsti	steel
nik	Steel.SpinLock.fst	steel
nik	Steel.SpinLock.fsti	steel
aymeric	Steel.SteelAtomic.Basics.fst	steel
nik/aymeric	Steel.SteelT.Basics.fst	steel
nik/aymeric	Steel.SteelT.Basics.fsti	steel