formal verification intro at minifest

minifest-tutorial.lean

import Lean.PrettyPrinter.Parenthesizer

/-
  live code in your own session
-/
#print Nat.rec

inductive tree (A : Type) : Type where
| leaf : A -> tree A
| node : tree A -> tree A -> tree A

#print tree.rec

inductive even : Nat -> Prop where
| ev0 : even 0
| evSS : forall n, even n -> even (n + 2)

#print even.rec

example : forall n, even n -> exists k, n = 2 * k := by
  intros n h
  induction h with
  | ev0 => exists 0
  | evSS n h ih => 
    have ⟨k, h⟩ := ih
    exists (k + 1)
    omega

/- 
  Shallow embedding imperative programming in lean
-/

/-- Unary operators -/
inductive UnOp where
  | neg
  | not
deriving Repr, DecidableEq

/-- Binary operators -/
inductive BinOp where
  | plus | minus | times | div
  | and | or
  | lt | le | eq
deriving Repr, DecidableEq

/-- Expressions -/
inductive Expr where
  | constInt (i : Int)
  | var (name : String)
  | un (op : UnOp) (e : Expr)
  | bin (op : BinOp) (e1 e2 : Expr)
deriving Repr, DecidableEq

/-- An environment maps variables names to their values (no pointers) -/
def Env := String → Int

namespace Env

/-- Set a value in an environment -/
def set (x : String) (v : Int) (σ : Env) : Env :=
  fun y => if x == y then v else σ y

def setOption (x : String) (v : Option Int) (σ : Env) : Env :=
  match v with
  | some v => σ.set x v
  | none => σ

/-- Look up a value in an environment -/
def get (x : String) (σ : Env) : Int :=
  σ x

/-- Initialize an environment, setting all uninitialized memory to `i` -/
def init (i : Int) : 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

/-- Helper that implements unary operators -/
def UnOp.apply : UnOp → Int → Option Int
  | .neg, i => Int.neg <$> some i
  | .not, b => if b == 0 then some 1 else some 0

/-- Helper that implements binary operators -/
def BinOp.apply : BinOp → Int → Int → Option Int
  | .plus, i, j => some $ (i + j)
  | .minus, i, j => some $ (i - j)
  | .times, i, j => some $ (i * j)
  | .div, i, j => if j == 0 then none else some $ (i / j)
  | .and, b, c => some $ (b * c)
  | .or, b, c => some $ (b + c)
  | .eq, i, j => some $ if i == j then 1 else 0
  | .le, i, j => some (if i <= j then 1 else 0)
  | .lt, i, j => some $ if i < j then 1 else 0

/--
Evaluates an expression, finding the value if it has one.

Expressions that divide by zero don't have values - the result is undefined.
-/
def Expr.eval (σ : Env) : Expr → Option Int
  | .constInt i => some i
  | .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


/- 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 -/
open Lean PrettyPrinter Parenthesizer in
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

/-- Strings -/
syntax:1 "[" str "]": 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

/-- 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

/-- 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.constInt $(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 .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.
open Lean PrettyPrinter Parenthesizer in
@[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)

namespace Imp

/-- Statements in Imp -/
inductive Stmt where
  /-- A statement that does nothing -/
  | skip
  /-- Executes `stmt1` then `stmt2` -/
  | seq (stmt1 stmt2 : Stmt)
  /-- Modifies a variable in the state -/
  | assign (name : String) (val : Expr)
  /--
  Conditional: executes `ifTrue` when `cond`'s value is nonzero, `ifFalse` otherwise
  -/
  | if (cond : Expr) (ifTrue ifFalse : Stmt)
  /--
  Repeats `body` as long as `cond` evaluates to a nonzero value
  -/
  | while (cond : Expr) (body : Stmt)
deriving Repr, DecidableEq

#print Stmt.rec

/-- Imp statements -/
declare_syntax_cat stmt
/-- A statement that does nothing -/
syntax "skip" ";" : stmt
/-- Sequencing: one statement after another -/
syntax stmt ppDedent(ppLine stmt) : stmt
/-- Assignment -/
syntax varname " := " exp ";" : stmt
/-- Conditional statement -/
syntax "if " "(" exp ")" ppHardSpace "{" ppLine stmt ppDedent(ppLine "}" ppHardSpace "else" ppHardSpace "{") ppLine stmt ppDedent(ppLine "}") : stmt
/-- Loop -/
syntax "while " "(" exp ")" ppHardSpace "{" ppLine stmt ppDedent(ppLine "}") : stmt
/-- Escape to Lean -/
syntax:max "~" term:max : stmt

/-- Include an Imp statement in Lean code -/
syntax:min "imp" ppHardSpace "{" ppLine stmt ppDedent(ppLine "}") : term

/-
The above rules are equivalent to the following, but with nicer-looking compiler output:

syntax "skip" ";" : stmt
syntax stmt stmt : stmt
syntax varname " := " exp ";" : stmt
syntax "if " "(" exp ") " "{" stmt "}" "else" "{" stmt "}" : stmt
syntax "while " "(" exp ") "  "{" stmt "}" : stmt
syntax:max "~" term:max : stmt

syntax:min "imp" "{" stmt "}" : term
-/


open Lean in
macro_rules
  | `(imp { skip; }) =>
    `(Stmt.skip)
  | `(imp { $s1 $s2 }) =>
    `(Stmt.seq (imp {$s1}) (imp {$s2}))
  | `(imp { $x:varname := $e;}) =>
    `(Stmt.assign (var {$x}) (expr {$e}))
  | `(imp { if ($c) {$s1} else {$s2} }) =>
    `(Stmt.if (expr{$c}) (imp{$s1}) (imp{$s2}))
  | `(imp { while ($c) {$s} }) =>
    `(Stmt.while (expr{$c}) (imp{$s}))
  | `(imp { ~$stx }) =>
    pure stx

/--
Truthiness: the result of evaluating an expression is "truthy" if it's defined and non-zero.
-/
def Truthy (v : Option Int) : Prop :=
  match v with
  | some x => x ≠ 0
  | none => False

instance : Decidable (Truthy v) :=
  match v with
  | some x => if h : x ≠ 0 then .isTrue h else .isFalse h
  | none => .isFalse id

@[simp]
theorem Truthy.some_nonzero : Truthy (some v) = (v ≠ 0) := by
  simp [Truthy]

@[simp]
theorem Truthy.not_none : Truthy none = False := by
  simp [Truthy]

@[simp]
theorem Truthy.eval_const_int : Truthy (Expr.eval σ (.constInt v)) = (v ≠ 0) := by
  simp [Truthy, Expr.eval]

/--
Falsiness: the result of evaluating an expression is "falsy" if it's 0
-/
def Falsy (v : Option Int) : Prop := match v with
  | some x => x = 0
  | none => False

@[simp]
theorem Falsy.eval_const_int : Falsy (Expr.eval σ (.constInt v)) = (v = 0) := by
  simp [Falsy, Expr.eval]

@[simp]
theorem Falsy.some_zero : Falsy (some v) = (v = 0) := by
  simp [Falsy]

@[simp]
theorem Falsy.not_none : Falsy none = False := by
  simp [Falsy]

def Int.truthy : Int → Prop
  | x => x ≠ 0

instance : Decidable (Falsy v) :=  -- inferInstanceAs (Decidable (v = 0))
  match v with
  | some x => if h : x = 0 then .isTrue h else .isFalse h
  | none => .isFalse id

theorem Truthy.not_falsy : Truthy v → ¬Falsy v := by
  intro h1 h2
  simp [Truthy, Falsy] at *
  cases v <;> simp at *
  case some v =>
    cases v <;> simp at *
    contradiction

namespace Stmt

/--
Big-step semantics: `BigStep σ s σ'` means that running the program `s` in the starting state `σ` is
termination with the final state `σ'`.
-/
inductive BigStep : Env → Stmt → Env → Prop where
  | skip :
    BigStep σ (imp {skip;}) σ
  | seq :
    BigStep σ s1 σ' → BigStep σ' s2 σ'' →
    BigStep σ (imp{ ~s1 ~s2}) σ''
  | assign :
    e.eval σ = some v →
    BigStep σ (imp {~x := ~e;}) (σ.set x v)
  | ifTrue :
    Truthy (c.eval σ) → BigStep σ s1 σ' →
    BigStep σ (imp {if (~c) {~s1} else {~s2}}) σ'
  | ifFalse :
    Falsy (c.eval σ) → BigStep σ s2 σ' →
    BigStep σ (imp {if (~c) {~s1} else {~s2}}) σ'
  | whileTrue :
    Truthy (c.eval σ) →
    BigStep σ body σ' →
    BigStep σ' (imp {while (~c) {~body}}) σ'' →
    BigStep σ (imp {while (~c) {~body}}) σ''
  | whileFalse :
    Falsy (c.eval σ) →
    BigStep σ (imp {while (~c) {~body}}) σ

attribute [simp] BigStep.skip

syntax term:60 " / " term:61 " ↓ " term:62 : term
macro_rules
  | `($s / $σ ↓ $σ') => `(BigStep $σ $s $σ')

@[simp]
def ValidHoareTriple (P : Env → Prop) (c : Stmt) (Q : Env → Prop) : Prop :=
  forall (st st' : Env), P st -> c / st ↓ st' -> Q st'

syntax "{{" term:90 "}} " term:91 " {{" term:92 "}}" : term
macro_rules
  | `({{$P}}$c{{$Q}}) => `(ValidHoareTriple $P $c $Q)

def increment : Stmt := imp { x := x + 1; }

@[simp] def increment_spec : Prop := {{fun (st : Env) => st.get "x" < 1}}increment{{fun st => st.get "x" < 2}}

theorem increment_correct : increment_spec := by
  simp [ValidHoareTriple]
  intros st st' hP h
  cases h with
  | assign h3 =>
    simp [Expr.eval, BinOp.apply] at h3
    cases h3
    simp [Env.get, Env.set] at *
    omega