F* Documentation

Pulse is a domain-specific language (DSL) embedded in F*. It inherits F*'s higher-order features and dependent types while providing built-in support for programming with mutable state and concurrency. Pulse uses specifications and proofs based on Concurrent Separation Logic (CSL).

Key characteristics:

• Embedded in F*: Uses F*'s lemmas, dependent types, and refinement types.
• Concurrency Support: Built-in primitives for parallel execution (e.g., the par combinator).
• Logic Foundation: Based on PulseCore, a logic formalized within F* that is inspired by the Iris separation logic.

F* is a dependently typed programming language designed for several roles:

• General-purpose programming: Encourages higher-order functional programming with effects (ML family tradition).
• Compiler: Translates F* programs to OCaml, F#, C, or Wasm.
• Proof assistant: Used to state and prove properties of programs.
• Program verification engine: Leverages SMT solvers to partially automate proofs.
• Metaprogramming system: Supports programmatic construction of F* programs and proof automation.

Key design elements include a core language of total functions with full dependent types, a system of user-defined indexed effects, built-in encoding of logic for SMT solvers, and a reflection system for metaprogramming (Meta-F*).

F* is a dependently typed programming language and proof assistant designed for proof-oriented programming. This paradigm involves co-designing programs and proofs to provide mathematical guarantees regarding:

• Functional correctness: Precisely characterizing input/output behavior.
• Security properties: Ensuring programs do not leak secrets.
• Resource usage: Providing bounds on how resources are consumed.

While F* is a functional language at its core, it supports multiple programming paradigms including:

• Pure, total functions.
• Low-level programming (e.g., C and assembly).
• Concurrent programming (shared memory and message-passing).
• Distributed programming.

F* supports first-class functions, allowing for higher-order patterns:

• map: Takes a function f and a list l, applying f to every element to produce a new list.
• find: Takes a predicate function f and a list l, returning Some x for the first element where f x is true, or None if no such element exists.
• fold_left: Reduces a list using a function f and an accumulator a from left to right.

In F*, logical connectives exist in two flavors:

1. Constructive: Defined as inductive or arrow types. These provide a direct way to build and manipulate proofs using standard type theory (e.g., pair for conjunction, sum for disjunction).
2. Propositional (Classical): Represented by symbols like `/

, /, ==>`, etc. These are typically used in proofs where the SMT solver handles the heavy lifting. Their meaning is determined by SMT encoding rather than explicit constructors.

All basic types and connectives are defined in the Prims module, which is the first module in all F* programs.

F* uses an effect system to model behaviors beyond pure mathematical functions. While users can define custom effects, F* provides several primitive effects to manage specific computational behaviors:

• Ghost: Describes parts of a program with no observable behavior that do not influence the returned result. This allows the compiler to erase computationally irrelevant parts during optimization.
• Divergence: Encapsulates computations that may run forever. The effect system ensures that potentially divergent computations cannot be used as proofs.
• Partiality: Represents partial functions that are only defined over a subset of their domain.

Pulse supports three kinds of mutable references for explicit memory management:

1. Stack references: Allocated in the current function's stack frame and implicitly reclaimed when the function returns.
2. Heap references (boxes): Allocated in the heap and must be explicitly reclaimed using drop or free.
3. Ghost references: Used exclusively for specification and proof; they do not exist at runtime.

The basic type for mutable references is Pulse.Lib.Reference.ref t. Most operations are agnostic to whether the reference is on the stack or the heap.

The tutorial defines a small imperative language used to demonstrate Floyd-Hoare logic. The language includes:

• Expressions: Integer constants, global variables (natural numbers), and arithmetic (e.g., addition).
• Assignments (EAssign x e): Assigns the result of expression e to global variable x.
• Sequence (Seq): Composes programs sequentially.
• Conditional (If): Composes programs conditionally.
• Repeat (Repeat n p): A primitive recursion construct that repeats program p, n times (where n is a non-negative integer).

Operational semantics are implemented via an interpreter using a state type and a state monad st a. The interpreter is a total, recursive function run of type st unit.