it begins

.github/workflows/lean_action_ci.yml

@@ -0,0 +1,16 @@
+name: Lean Action CI
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+      - uses: leanprover/lean-action@v1
+        with:
+          lake-package-directory: imp

README.md

@@ -0,0 +1 @@
+# Formally Verified APPS

imp/.gitignore

@@ -0,0 +1 @@
+/.lake

imp/Imp.lean

@@ -0,0 +1,2 @@
+import Imp.Expr
+import Imp.Stmt

imp/Imp/Expr.lean

@@ -0,0 +1,7 @@
+/-
+This file exists only to re-export the contents of the `Imp.Expr` module hierarchy.
+-/
+import Imp.Expr.Basic
+import Imp.Expr.Delab
+import Imp.Expr.Eval
+import Imp.Expr.Syntax

imp/Imp/Expr/Basic.lean

@@ -0,0 +1,27 @@
+namespace Imp.Expr
+
+/-- Unary operators -/
+inductive UnOp where
+  | neg
+  | not
+deriving Repr, DecidableEq
+
+/-- Binary operators -/
+inductive BinOp where
+  | plus | minus | times | div
+  | and | or
+  | lt | le | eq
+  | append
+deriving Repr, DecidableEq
+
+end Expr
+
+/-- Expressions -/
+inductive Expr where
+  | constInt (i : Int)
+  | constStr (x : String)
+  | constBool (x : Bool)
+  | var (name : String)
+  | un (op : Expr.UnOp) (e : Expr)
+  | bin (op : Expr.BinOp) (e1 e2 : Expr)
+deriving Repr, DecidableEq

imp/Imp/Expr/Delab.lean

@@ -0,0 +1,110 @@
+/-
+This file makes the convenient syntax from `Imp.Expr.Syntax` show up in Lean's output. It's not part
+of what's being taught in the lectures.
+-/
+import Lean.PrettyPrinter.Delaborator
+import Imp.Expr.Basic
+import Imp.Expr.Syntax
+
+open Lean PrettyPrinter Delaborator SubExpr Parenthesizer
+
+namespace Imp.Expr.Delab
+
+def annAsTerm {any} (stx : TSyntax any) : DelabM (TSyntax any) :=
+  (⟨·⟩) <$> annotateTermInfo ⟨stx.raw⟩
+
+def delabNameInner : DelabM (TSyntax `varname) := do
+  let e ← getExpr
+  match e with
+  | .lit (.strVal s) =>
+    let x := mkIdent <| .mkSimple s
+    pure <| ⟨x.raw⟩
+  | _ => `(varname|~($(← delab))) >>= annAsTerm
+
+partial def delabExprInner : DelabM (TSyntax `exp) := do
+  let e ← getExpr
+  let stx ←
+    match_expr e with
+    | Expr.constInt x =>
+      match_expr x with
+      | OfNat.ofNat _ n _ =>
+        if let some n' := n.nat? then
+          pure <| ⟨Syntax.mkNumLit (toString n') |>.raw⟩
+        else if let .lit (.natVal n') := n then
+          pure <| ⟨Syntax.mkNumLit (toString n') |>.raw⟩
+        else withAppArg `(exp| ~$(← delab))
+      | Int.ofNat n =>
+        if let some n' := n.nat? then
+          pure <| ⟨Syntax.mkNumLit (toString n') |>.raw⟩
+        else if let .lit (.natVal n') := n then
+          pure <| ⟨Syntax.mkNumLit (toString n') |>.raw⟩
+        else withAppArg `(exp| ~$(← delab))
+      | BitVec.ofNat _ _ => (⟨·.raw⟩) <$> (withAppArg <| withAppArg <| delab)
+      | _ =>
+        `(exp| ~(Expr.const $(← withAppArg delab)))
+    | Expr.var _ => do
+      let x ← withAppArg delabNameInner
+      `(exp|$x:varname)
+    | Expr.bin op _ _ =>
+      let s1 ← withAppFn <| withAppArg delabExprInner
+      let s2 ← withAppArg delabExprInner
+      match_expr op with
+      | BinOp.plus => `(exp| $s1 + $s2)
+      | BinOp.minus => `(exp| $s1 - $s2)
+      | BinOp.times => `(exp| $s1 * $s2)
+      | BinOp.div => `(exp| $s1 / $s2)
+      | BinOp.and => `(exp| $s1 && $s2)
+      | BinOp.or => `(exp| $s1 || $s2)
+      | BinOp.lt => `(exp| $s1 < $s2)
+      | BinOp.le => `(exp| $s1 ≤ $s2)
+      | BinOp.eq => `(exp| $s1 == $s2)
+      | _ => `(exp|~(Expr.bin $(← withAppFn <| withAppFn <| withAppArg delab) $(← withAppFn <| withAppArg delab) $(← withAppArg delab)))
+    | Expr.un op _ =>
+      let s ← withAppArg delabExprInner
+      match_expr op with
+      | UnOp.neg => `(exp|-$s)
+      | UnOp.not => `(exp|!$s)
+      | _ => `(exp| ~(Expr.un $(← withAppFn <| withAppArg delab) $(← withAppArg delab)))
+    | _ =>
+      `(exp| ~$(← delab))
+  annAsTerm stx
+
+@[delab app.Imp.Expr.const, delab app.Imp.Expr.var, delab app.Imp.Expr.un, delab app.Imp.Expr.bin]
+partial def delabExpr : Delab := do
+  -- This delaborator only understands a certain arity - give up if it's incorrect
+  guard <| match_expr ← getExpr with
+    | Expr.const _ => true
+    | Expr.var _ => true
+    | Expr.un _ _ => true
+    | Expr.bin _ _ _ => true
+    | _ => false
+  match ← delabExprInner with
+  | `(exp|~$e) => pure e
+  | e => `(term|expr {$(⟨e⟩)})
+
+/-- info: expr { 5 } : Expr -/
+#guard_msgs in
+#check Expr.constInt 5
+
+/-- info: expr { 5 } : Expr -/
+#guard_msgs in
+#check expr { 5 }
+
+/-- info: expr { x } : Expr -/
+#guard_msgs in
+#check expr { x }
+
+/-- info: expr { 5 + 23 - 10 } : Expr -/
+#guard_msgs in
+#check expr { 5 + 23 - 10 }
+
+/-- info: expr { 5 + (23 - 10) } : Expr -/
+#guard_msgs in
+#check expr { 5 + (23 - 10) }
+
+/--
+info: let x := expr { 23 };
+expr { ~x * ~x } : Expr
+-/
+#guard_msgs in
+#check let x := expr {23}; expr {~x * ~x}

imp/Imp/Expr/Eval.lean

@@ -0,0 +1,86 @@
+import Imp.Expr.Basic
+
+open Lean
+
+namespace Imp
+
+inductive Value where
+| str : String -> Value
+| int : Int -> Value
+| bool : Bool -> Value
+
+instance : OfNat Value n := by
+  constructor
+  exact (Value.int n)
+
+/-- An environment maps variables names to their values (no pointers) -/
+def Env := String → Value
+
+namespace Env
+
+/-- Set a value in an environment -/
+def set (x : String) (v : Value) (σ : Env) : Env :=
+  fun y => if x == y then v else σ y
+
+/-- Look up a value in an environment -/
+def get (x : String) (σ : Env) : Value :=
+  σ x
+
+/-- Initialize an environment, setting all uninitialized memory to `i` -/
+def init (i : Value) : Env := fun _ => i
+
+@[simp]
+theorem get_init : (Env.init v).get x = v := by rfl
+
+@[simp]
+theorem get_set_same {σ : Env} : (σ.set x v).get x = v := by
+  simp [get, set]
+
+@[simp]
+theorem get_set_different {σ : Env} : x ≠ y → (σ.set x v).get y = σ.get y := by
+  intros
+  simp [get, set, *]
+
+end Env
+
+namespace Expr
+
+/-- Helper that implements unary operators -/
+def UnOp.apply : UnOp → Value → Option Value
+  | .neg, .int i => (Value.int ∘ Int.neg) <$> some i
+  | .not, .bool b => (Value.bool ∘ Bool.not) <$> some b
+  | _, _ => none
+
+/-- Helper that implements binary operators -/
+def BinOp.apply : BinOp → Value → Value → Option Value
+  | .plus, .int i, .int j => some $ Value.int (i + j)
+  | .minus, .int i, .int j => some $ Value.int (i - j)
+  | .times, .int i, .int j => some $ Value.int (i * j)
+  | .div, .int i, .int j => if j == 0 then none else some $ Value.int (i / j)
+  | .and, .bool b, .bool c => some $ Value.bool (b && c)
+  | .or, .bool b, .bool c => some $ Value.bool (b || c)
+  | .eq, .int i, .int j => some $ Value.bool (i == j)
+  | .eq, .bool b, .bool c => some $ Value.bool (b == c)
+  | .eq, .str s, .str t => some $ Value.bool (s == t)
+  | .le, .int i, .int j => some $ Value.bool (i <= j)
+  | .lt, .int i, .int j => some $ Value.bool (i < j)
+  |.append, .str s, .str t => some $ Value.str (s ++ t)
+  | _, _, _ => none
+
+/--
+Evaluates an expression, finding the value if it has one.
+
+Expressions that divide by zero don't have values - the result is undefined.
+-/
+def eval (σ : Env) : Expr → Option Value
+  | .constInt i => some $ Value.int i
+  | .constBool b => some $ .bool b
+  | .constStr s => some $ .str s
+  | .var x => σ.get x
+  | .un op e => do
+    let v ← e.eval σ
+    op.apply v
+  | .bin op e1 e2 => do
+    let v1 ← e1.eval σ
+    let v2 ← e2.eval σ
+    op.apply v1 v2

imp/Imp/Expr/Syntax.lean

@@ -0,0 +1,126 @@
+import Lean.PrettyPrinter.Parenthesizer
+import Imp.Expr.Basic
+
+namespace Imp.Expr
+
+open Lean PrettyPrinter Parenthesizer
+
+
+/- Add a new nonterminal to Lean's grammar, called `varname` -/
+/-- Variable names in Imp -/
+declare_syntax_cat varname
+
+/- There are two productions: identifiers and antiquoted terms -/
+syntax ident : varname
+syntax:max "~" term:max : varname
+
+/- `varname`s are included in terms using `var { ... }`, which is a hook on which to hang the macros
+that translate the `varname` syntax into ordinary Lean expressions. -/
+syntax "var " "{" varname "}" : term
+
+/- These macros translate each production of the `varname` nonterminal into Lean expressions -/
+macro_rules
+  | `(var { $x:ident }) => `(term|$(quote x.getId.toString))
+  | `(var { ~$stx }) => pure stx
+
+/-- Expressions in Imp -/
+declare_syntax_cat exp
+
+/-- Variable names -/
+syntax varname : exp
+
+/-- Numeric constant -/
+syntax num : exp
+
+/-- Arithmetic complement -/
+syntax:75 "-" exp:75 : exp
+
+/-- Multiplication -/
+syntax:70 exp:70 " * " exp:71 : exp
+/-- Division -/
+syntax:70 exp:70 " / " exp:71 : exp
+
+/-- Addition -/
+syntax:65 exp:65 " + " exp:66 : exp
+/-- Subtraction -/
+syntax:65 exp:65 " - " exp:66 : exp
+
+/-- Left shift -/
+syntax:55 exp:55 " <<< " exp:56 :exp
+/-- Right shift -/
+syntax:55 exp:55 " >>> " exp:56 :exp
+
+/-- Boolean negation -/
+syntax:75 "!" exp:75 : exp
+/-- Less than -/
+syntax:50 exp:50 " < " exp:51 : exp
+/-- Less than or equal to -/
+syntax:50 exp:50 " ≤ " exp:51 : exp
+/-- Greater than or equal to -/
+syntax:50 exp:50 " ≥ " exp:51 : exp
+/-- Greater than -/
+syntax:50 exp:50 " > " exp:51 : exp
+/-- Equal -/
+syntax:45 exp:45 " == " exp:46 : exp
+
+/-- Bitwise and -/
+syntax:40 exp:40 " &&& " exp:41 :exp
+/-- Bitwise or -/
+syntax:40 exp:40 " ||| " exp:41 :exp
+
+/-- Boolean conjunction -/
+syntax:35 exp:35 " && " exp:36 : exp
+/-- Boolean disjunction -/
+syntax:35 exp:35 " || " exp:36 : exp
+
+/-- Parentheses for grouping -/
+syntax "(" exp ")" : exp
+
+/-- Escape to Lean -/
+syntax:max "~" term:max : exp
+
+/-- Embed an Imp expression into a Lean expression -/
+syntax:min "expr " "{ " exp " }" : term
+
+open Lean in
+macro_rules
+  | `(expr{$x:ident}) => `(Expr.var $(quote x.getId.toString))
+  | `(expr{$n:num}) => `(Expr.const $(quote n.getNat))
+
+  | `(expr{-$e}) => `(Expr.un .neg (expr{$e}))
+  | `(expr{!$e}) => `(Expr.un .not (expr{$e}))
+
+  | `(expr{$e1 + $e2}) => `(Expr.bin .plus (expr{$e1}) (expr{$e2}))
+  | `(expr{$e1 * $e2}) => `(Expr.bin .times (expr{$e1}) (expr{$e2}))
+  | `(expr{$e1 - $e2}) => `(Expr.bin .minus (expr{$e1}) (expr{$e2}))
+  | `(expr{$e1 / $e2}) => `(Expr.bin .div (expr{$e1}) (expr{$e2}))
+
+  | `(expr{$e1 >>> $e2}) => `(Expr.bin .rsh (expr{$e1}) (expr{$e2}))
+  | `(expr{$e1 <<< $e2}) => `(Expr.bin .lsh (expr{$e1}) (expr{$e2}))
+  | `(expr{$e1 ||| $e2}) => `(Expr.bin .bor (expr{$e1}) (expr{$e2}))
+  | `(expr{$e1 &&& $e2}) => `(Expr.bin .band (expr{$e1}) (expr{$e2}))
+
+
+  | `(expr{$e1 && $e2}) => `(Expr.bin .and (expr{$e1}) (expr{$e2}))
+  | `(expr{$e1 || $e2}) => `(Expr.bin .or (expr{$e1}) (expr{$e2}))
+
+  | `(expr{$e1 < $e2}) => `(Expr.bin .lt (expr{$e1}) (expr{$e2}))
+  | `(expr{$e1 ≤ $e2}) => `(Expr.bin .le (expr{$e1}) (expr{$e2}))
+  | `(expr{$e1 == $e2}) => `(Expr.bin .eq (expr{$e1}) (expr{$e2}))
+  | `(expr{$e1 ≥ $e2}) => `(Expr.bin .le (expr{$e2}) (expr{$e1}))
+  | `(expr{$e1 > $e2}) => `(Expr.bin .lt (expr{$e2}) (expr{$e1}))
+  | `(expr{($e)}) => `(expr{$e})
+  | `(expr{~$stx}) => pure stx
+
+
+-- Copied from Lean's term parenthesizer - applies the precedence rules in the grammar to add
+-- parentheses as needed. This isn't needed when adding new input syntax to Lean, but because the
+-- file `Delab.lean` makes Lean use this syntax in its output, the parentheses are needed.
+@[category_parenthesizer exp]
+def exp.parenthesizer : CategoryParenthesizer | prec => do
+  maybeParenthesize `exp true wrapParens prec $
+    parenthesizeCategoryCore `exp prec
+where
+  wrapParens (stx : Syntax) : Syntax := Unhygienic.run do
+    let pstx ← `(($(⟨stx⟩)))
+    return pstx.raw.setInfo (SourceInfo.fromRef stx)

imp/Imp/Stmt.lean

@@ -0,0 +1,7 @@
+/-
+This file exists only to re-export the contents of the `Imp.Stmt` module hierarchy.
+-/
+import Imp.Stmt.Basic
+import Imp.Stmt.BigStep
+import Imp.Stmt.Delab
+import Imp.Stmt.Optimize