Strata language definition document (#186)

Adds a document describing the semantics of Strata Core (consisting of
`Lambda` and `Imperative` components). The document is written in Verso
and imports the Strata library to allow docstrings to appear directly in
the text.

Note that Strata Core is not a new dialect, but rather a new name for
the combination of `Lambda` and `Imperative`. It does not yet have a
concrete syntax. Concrete syntax will likely be provided through an
evolution of #224, to assist in the goal of keeping Strata Core as close
to B3 as possible.

By submitting this pull request, I confirm that you can use, modify,
copy, and redistribute this contribution, under the terms of your
choice.

---------

Co-authored-by: Josh Cohen <cohenjo@amazon.com>
Co-authored-by: Mikaël Mayer <MikaelMayer@users.noreply.github.com>
Co-authored-by: Shilpi Goel <shigoel@gmail.com>
Co-authored-by: Andrew Wells <130512013+andrewmwells-amazon@users.noreply.github.com>

Author: 5 people

.github/workflows/ci.yml

@@ -116,7 +116,7 @@ jobs:
         run: .github/scripts/checkLeanImport.sh
 
   build_doc:
-    name: Build Documentation
+    name: Build documentation
     runs-on: ubuntu-latest
     permissions:
       contents: read
@@ -126,10 +126,10 @@ jobs:
         uses: leanprover/lean-action@v1
         with:
           build-args: '--wfail'
-          lake-package-directory: 'docs/ddm'
-      - name: Build Documentation
-        run: lake exe docs 
-        working-directory: docs/ddm
+          lake-package-directory: 'docs/verso'
+      - name: Build documentation
+        run: ./generate.sh
+        working-directory: docs/verso
 
   build_python:
     name: Build and test Python

Strata/DL/Imperative/Cmd.lean

@@ -28,19 +28,22 @@ variable declaration and assignment, and assertions and assumptions.
 -/
 
 /--
-A command in the Imperative dialect
+A an atomic command in the `Imperative` dialect.
+
+Commands don't create local control flow, and are typically used as a parameter
+to `Imperative.Stmt` or other similar types.
 -/
 inductive Cmd (P : PureExpr) : Type where
-  /-- `init` defines a variable called `name` with type `ty` and
-    initial value `e`. -/
+  /-- Define a variable called `name` with type `ty` and initial value `e`.
+  Note: we may make the initial value optional. -/
   | init     (name : P.Ident) (ty : P.Ty) (e : P.Expr) (md : (MetaData P) := .empty)
-  /-- `set` assigns `e` to a pre-existing variable `name`. -/
+  /-- Assign `e` to a pre-existing variable `name`. -/
   | set      (name : P.Ident) (e : P.Expr) (md : (MetaData P) := .empty)
-  /-- `havoc` assigns a pre-existing variable `name` a random value. -/
+  /-- Assigns an arbitrary value to an existing variable `name`. -/
   | havoc    (name : P.Ident) (md : (MetaData P) := .empty)
-  /-- `assert` checks whether condition `b` is true. -/
+  /-- Check whether condition `b` is true, failing if not. -/
   | assert   (label : String) (b : P.Expr) (md : (MetaData P) := .empty)
-  /-- `assume` constrains execution by adding assumption `b`. -/
+  /-- Ignore any execution state in which `b` is not true. -/
   | assume   (label : String) (b : P.Expr) (md : (MetaData P) := .empty)
 
 abbrev Cmds (P : PureExpr) := List (Cmd P)

Strata/DL/Imperative/CmdSemantics.lean

@@ -234,10 +234,15 @@ def WellFormedSemanticEvalVar {P : PureExpr} [HasFvar P] (δ : SemanticEval P)
 
 def WellFormedSemanticEvalExprCongr {P : PureExpr} [HasVarsPure P P.Expr] (δ : SemanticEval P)
     : Prop := ∀ e σ σ', (∀ x ∈ HasVarsPure.getVars e, σ x = σ' x) → δ σ e = δ σ' e
+
 /--
-An inductive rule for state update.
+Abstract variable update.
+
+This does not specify how `σ` is represented, only what it maps each variable to.
 -/
 inductive UpdateState : SemanticStore P → P.Ident → P.Expr → SemanticStore P → Prop where
+  /-- The state `σ'` is be equivalent to `σ` except at `x`, where it maps to
+  `v`. Requires that `x` mapped to something beforehand. -/
   | update :
     σ x = .some v' →
     σ' x = .some v →
@@ -246,9 +251,13 @@ inductive UpdateState : SemanticStore P → P.Ident → P.Expr → SemanticStore
     UpdateState σ x v σ'
 
 /--
-An inductive rule for state init.
+Abtract variable initialization.
+
+This does not specify how `σ` is represented, only what it maps each variable to.
 -/
 inductive InitState : SemanticStore P → P.Ident → P.Expr → SemanticStore P → Prop where
+  /-- The state `σ'` is be equivalent to `σ` except at `x`, where it maps to
+  `v`. Requires that `x` mapped to nothing beforehand. -/
   | init :
     σ x = none →
     σ' x = .some v →
@@ -257,37 +266,43 @@ inductive InitState : SemanticStore P → P.Ident → P.Expr → SemanticStore P
     InitState σ x v σ'
 
 /--
-An inductively-defined operational semantics that depends on
-environment lookup and evaluation functions for expressions.
+An inductively-defined operational semantics for `Cmd` that depends on variable
+lookup (`σ`) and expression evaluation (`δ`) functions.
 -/
 inductive EvalCmd [HasFvar P] [HasBool P] [HasNot P] :
   SemanticEval P → SemanticStore P → Cmd P → SemanticStore P → Prop where
+  /-- If `e` evaluates to a value `v`, initialize `x` according to `InitState`. -/
   | eval_init :
     δ σ e = .some v →
     InitState P σ x v σ' →
     WellFormedSemanticEvalVar δ →
     ---
     EvalCmd δ σ (.init x _ e _) σ'
 
+  /-- If `e` evaluates to a value `v`, assign `x` according to `UpdateState`. -/
   | eval_set :
     δ σ e = .some v →
     UpdateState P σ x v σ' →
     WellFormedSemanticEvalVar δ →
     ----
     EvalCmd δ σ (.set x e _) σ'
 
+  /-- Assign `x` an arbitrary value `v` according to `UpdateState`. -/
   | eval_havoc :
     UpdateState P σ x v σ' →
     WellFormedSemanticEvalVar δ →
     ----
     EvalCmd δ σ (.havoc x _) σ'
 
+  /-- If `e` evaluates to true in `σ`, evaluate to the same `σ`. This semantics
+  does not have a concept of an erroneous execution. -/
   | eval_assert :
     δ σ e = .some HasBool.tt →
     WellFormedSemanticEvalBool δ →
     ----
     EvalCmd δ σ (.assert _ e _) σ
 
+  /-- If `e` evaluates to true in `σ`, evaluate to the same `σ`. -/
   | eval_assume :
     δ σ e = .some HasBool.tt →
     WellFormedSemanticEvalBool δ →

Strata/DL/Imperative/MetaData.lean

@@ -24,13 +24,15 @@ open Std (ToFormat Format format)
 
 variable {Identifier : Type} [DecidableEq Identifier] [ToFormat Identifier] [Inhabited Identifier]
 
-/-- A metadata field.
+/-- A metadata field, which can be either a variable or an arbitrary string label.
 
 For now, we only track the variables modified by a construct, but we will expand
 this in the future.
 -/
 inductive MetaDataElem.Field (P : PureExpr) where
+  /-- Metadata indexed by a Strata variable. -/
   | var (v : P.Ident)
+  /-- Metadata indexed by an arbitrary label. -/
   | label (l : String)
 
 @[grind]
@@ -61,9 +63,11 @@ instance [Repr P.Ident] : Repr (MetaDataElem.Field P) where
       | .label s => f!"MetaDataElem.Field.label {s}"
     Repr.addAppParen res prec
 
-/-- A metadata value. -/
+/-- A metadata value, which can be either an expression or a message. -/
 inductive MetaDataElem.Value (P : PureExpr) where
+  /-- Metadata value in the form of a structured expression. -/
   | expr (e : P.Expr)
+  /-- Metadata value in the form of an arbitrary string. -/
   | msg (s : String)
 
 instance [ToFormat P.Expr] : ToFormat (MetaDataElem.Value P) where
@@ -103,7 +107,9 @@ instance [DecidableEq P.Expr] : DecidableEq (MetaDataElem.Value P) :=
 
 /-- A metadata element -/
 structure MetaDataElem (P : PureExpr) where
+  /-- The field or key used to identify the metadata. -/
   fld   : MetaDataElem.Field P
+  /-- The value of the metadata. -/
   value : MetaDataElem.Value P
 
 /-- Metadata is an array of tagged elements. -/

Strata/DL/Imperative/NondetStmt.lean

@@ -22,10 +22,23 @@ Comamnds](https://en.wikipedia.org/wiki/Guarded_Command_Language), and in
 [Kleene Algebra with Tests](https://www.cs.cornell.edu/~kozen/Papers/kat.pdf).
 -/
 
+/--
+A non-deterministic statement, parameterized by a type of pure expressions (`P`)
+and a type of commands (`Cmd`).
+
+This encodes the same types of control flow as `Stmt`, but using only
+non-deterministic choices: arbitrarily choosing one of two sub-statements to
+execute or executing a sub-statement an arbitrary number of times. Conditions
+can be encoded if the command type includes assumptions.
+-/
 inductive NondetStmt (P : PureExpr) (Cmd : Type) : Type where
+  /-- An atomic command, of an arbitrary type. -/
   | cmd      (cmd : Cmd)
+  /-- Execute `s1` followed by `s2`. -/
   | seq      (s1 s2 : NondetStmt P Cmd)
+  /-- Execute either `s1` or `s2`, arbitrarily. -/
   | choice   (s1 s2 : NondetStmt P Cmd)
+  /-- Execute `s` an arbitrary number of times (possibly zero). -/
   | loop     (s : NondetStmt P Cmd)
   deriving Inhabited
 

Strata/DL/Imperative/NondetStmtSemantics.lean

@@ -14,8 +14,9 @@ namespace Imperative
 mutual
 
 /-- An inductively-defined operational semantics for non-deterministic
-statements that depends on environment lookup and evaluation functions
-for expressions.  -/
+statements that depends on environment lookup and evaluation functions for
+expressions.  **NOTE:** This will probably be replaced with a small-step
+semantics. -/
 inductive EvalNondetStmt (P : PureExpr) (Cmd : Type) (EvalCmd : EvalCmdParam P Cmd)
   [HasVarsImp P (List (Stmt P Cmd))] [HasVarsImp P Cmd] [HasFvar P] [HasBool P] [HasNot P] :
   SemanticEval P → SemanticStore P → NondetStmt P Cmd → SemanticStore P → Prop where

Strata/DL/Imperative/Stmt.lean

@@ -17,17 +17,30 @@ Imperative's Statements include commands and add constructs like structured and
 unstructured control-flow.
 -/
 
+/-- Imperative statements focused on control flow.
+
+The `P` parameter specifies the type of expressions that appear in conditional
+and loop guards.  The `Cmd` parameter specifies the type of atomic command
+contained within the `.cmd` constructor.
+-/
 inductive Stmt (P : PureExpr) (Cmd : Type) : Type where
+  /-- An atomic command. -/
   | cmd      (cmd : Cmd)
+  /-- An block containing a `List` of `Stmt`. -/
   | block    (label : String) (b : List (Stmt P Cmd)) (md : MetaData P := .empty)
-  /-- `ite` (if-then-else) statement provides structured control flow. -/
+  /-- A conditional execution statement. -/
   | ite      (cond : P.Expr)  (thenb : List (Stmt P Cmd)) (elseb : List (Stmt P Cmd)) (md : MetaData P := .empty)
-  /-- `loop` Loop statement with optional measure (for termination) and invariant. -/
+  /-- An iterated execution statement. Includes an optional measure (for
+  termination) and invariant. -/
   | loop     (guard : P.Expr) (measure : Option P.Expr) (invariant : Option P.Expr) (body : List (Stmt P Cmd)) (md : MetaData P := .empty)
-  /-- `goto` provides unstructured control flow. -/
+  /-- A semi-structured control flow statement transferring control to the given
+  label. The control flow induced by `goto` must not create cycles. **NOTE:**
+  This will likely be removed, in favor of an alternative view of imperative
+  programs that is purely untructured. -/
   | goto     (label : String) (md : MetaData P := .empty)
   deriving Inhabited
 
+/-- A block is simply an abbreviation for a list of commands. -/
 abbrev Block (P : PureExpr) (Cmd : Type) := List (Stmt P Cmd)
 
 def Stmt.isCmd {P : PureExpr} {Cmd : Type} (s : Stmt P Cmd) : Bool :=

Strata/DL/Imperative/StmtSemanticsSmallStep.lean

@@ -20,12 +20,15 @@ dialect's statement constructs.
 /--
 Configuration for small-step semantics, representing the current execution
 state. A configuration consists of:
-- The current statement being executed
+- The current statement (or list of statements) being executed
 - The current store
 -/
 inductive Config (P : PureExpr) (CmdT : Type) : Type where
+  /-- A single statement to execute next. -/
   | stmt : Stmt P CmdT → SemanticStore P → Config P CmdT
+  /-- A list of statements to execute next, in order. -/
   | stmts : List (Stmt P CmdT) → SemanticStore P → Config P CmdT
+  /-- A terminal configuration, indicating that execution has finished. -/
   | terminal : SemanticStore P → Config P CmdT
 
 /--
@@ -41,22 +44,22 @@ inductive StepStmt
   [HasBool P] [HasNot P] :
   SemanticEval P → SemanticStore P → Config P CmdT → Config P CmdT → Prop where
 
-  /-- Command: a command steps to terminal configuration if it
-  evaluates successfully -/
+  /-- A command steps to terminal configuration if it evaluates successfully -/
   | step_cmd :
     EvalCmd δ σ c σ' →
     ----
     StepStmt P EvalCmd δ σ
       (.stmt (.cmd c) σ)
       (.terminal σ')
 
-  /-- Block: a labeled block steps to its statement list -/
+  /-- A labeled block steps to its statement list. -/
   | step_block :
     StepStmt P EvalCmd δ σ
       (.stmt (.block _ ss _) σ)
       (.stmts ss σ)
 
-  /-- Conditional (true): if condition evaluates to true, step to then-branch -/
+  /-- If the condition of an `ite` statement evaluates to true, step to the then
+  branch. -/
   | step_ite_true :
     δ σ c = .some HasBool.tt →
     WellFormedSemanticEvalBool δ →
@@ -65,7 +68,8 @@ inductive StepStmt
       (.stmt (.ite c tss ess _) σ)
       (.stmts tss σ)
 
-  /-- Conditional (false): if condition evaluates to false, step to else-branch -/
+  /-- If the condition of an `ite` statement evaluates to false, step to the else
+  branch. -/
   | step_ite_false :
     δ σ c = .some HasBool.ff →
     WellFormedSemanticEvalBool δ →
@@ -74,7 +78,7 @@ inductive StepStmt
       (.stmt (.ite c tss ess _) σ)
       (.stmts ess σ)
 
-  /-- Loop (guard true): if guard is true, execute body then loop again -/
+  /-- If a loop guard is true, execute the body and then loop again. -/
   | step_loop_enter :
     δ σ g = .some HasBool.tt →
     WellFormedSemanticEvalBool δ →
@@ -83,7 +87,7 @@ inductive StepStmt
       (.stmt (.loop g m inv body md) σ)
       (.stmts (body ++ [.loop g m inv body md]) σ)
 
-  /-- Loop (guard false): if guard is false, terminate the loop -/
+  /-- If a loop guard is false, terminate the loop. -/
   | step_loop_exit :
     δ σ g = .some HasBool.ff →
     WellFormedSemanticEvalBool δ →
@@ -94,14 +98,14 @@ inductive StepStmt
 
   /- Goto: not implemented, because we plan to remove it. -/
 
-  /-- Empty statement list: no statements left to execute -/
+  /-- An empty list of statements steps to `.terminal` with no state changes. -/
   | step_stmts_nil :
     StepStmt P EvalCmd δ σ
       (.stmts [] σ)
       (.terminal σ)
 
-  /-- Statement composition: after executing a statement, continue with
-  remaining statements -/
+  /-- To evaluate a sequence of statements, evaluate the first statement and
+  then evaluate the remaining statements in the resulting state. -/
   | step_stmt_cons :
     StepStmt P EvalCmd δ σ (.stmt s σ) (.terminal σ') →
     ----

Strata/DL/Lambda/Identifiers.lean

@@ -20,7 +20,10 @@ section Identifiers
 Identifiers with a name and additional metadata
 -/
 structure Identifier (IDMeta : Type) : Type where
+  /-- A unique name. -/
   name : String
+  /-- Any additional metadata that it would be useful to attach to an
+  identifier. -/
   metadata : IDMeta
 deriving Repr, DecidableEq, Inhabited