Defining a simple stack langauge with Lean4

Published: 12-19-24

What is a stack language?

  • a “normal” programming language has functions on parameters. It is obvious what the parameters to each operation are.
    • ie max(10, 11) we know that there is some function max that takes two numbers (int, float, etc…)
  • however a stack language maintains (you guessed it) a stack of values and every operation interacts with these values based on their position in the stack.
    • most low level (lower than C / Rust) like assembly, jvm-bytecode and WASM are stack based languages (most assembly languages use registers but they can be thought of as “stack adjacent”).
    • when an operation requires values from the stack it “pops” them and “pushes” their result back onto the stack.
    • some operations with no parameters just push values onto the stack, such as declaring constants.
  • a course project included creating a simple imperative language and a verified compiler to WASM, however this post focuses on defining verified semantics for the subset of WASM used in this project.
  • a sample of a simple WASM program can be seen below
(module
    (func (export "_start") (result i32)
    ;; load 80 onto the stack
    i32.const 80
    ;; load 10 onto the stack
    i32.const 10
    ;; divide
    i32.div_u
    ;; return the last value of the stack [8]
    return
    )
)

Lean4

  • Lean is what is called a proof assistant
  • this means that it won’t prove things for you, but that you can use it to prove things.
    • ie it has functions / utilities for creating theorems and then incrementally proving them.
  • Lean is also a great functional language with all of the features that you would expect out of a modern functional first language.
    • macros
    • pattern matching
    • type classes
    • dependent types
  • the language is written in C++. Your proofs (theories) and functions compile down to a performant binary.
  • from the lean website

    Lean is a functional programming language that makes it easy to write correct and maintainable code. You can also use Lean as an interactive theorem prover.

  • for the last several decades the Coq proof assistant has dominated the programming language research landscape. However, Lean has taken hold in the mathematics community in the last few years and it’s my hope that it can start taking over PL as well!

Nix Flakes

  • because Lean is relatively new and the developers have stated that there will be breaking changes I decided to use Nix to create reproducible environments.
  • I am using Nix Flakes to create a devshell where I have pinned versions of a package installed and loaded into a new shell environment. Think virtual environments in python.
    • your first devshell will use a good deal of storage (1G) because Nix adds its versions of common core utils. However, every dev shell created after will use the cached versions of these core utils.
  • the shell is instantiated with nix develop
# This flake was initially generated by fh, the CLI for FlakeHub (version 0.1.18)
{
  # A helpful description of your flake
  description = "LeanEnv";

  # Flake inputs
  inputs = {
      nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable"; # package repo
  };

  # Flake outputs that other flakes can use
  outputs = { self, nixpkgs }:
    let
      # Helpers for producing system-specific outputs
      supportedSystems = [ "x86_64-linux" "aarch64-darwin" ];
      forEachSupportedSystem = f: nixpkgs.lib.genAttrs supportedSystems (system: f {
        pkgs = import nixpkgs { inherit system; };
      });
    in {
      # Development environments
      devShells = forEachSupportedSystem ({ pkgs }: {
        default = pkgs.mkShell {
          # Pinned packages available in the environment
          buildInputs = with pkgs; [
            lean4
          ];
        };
      });
    };
}

Project Outline

  1. define our context, the stack and state.
  2. define the syntax of our language.
  3. define the semantics of our language.
  4. prove our semantics are deterministic
    • same program with the same initial state results in the same end state
  • most of the explanation lives in the comments of the code I’m showing below.

state & stack

/-! 
- for Stack state is defined as a function from a string to an int
  - in essence this is a **total map**
  - we map strings to integer values
- we explicitly define `state` and `empty_state`
- we create custom notation for updating the *state map*
  - `∀ (st : state) (v : String) (x : Int), st[v !-> x]`
-/

/-! Define state as a function from String to Int -/
def state : Type :=
  String → Int

/-! Define empty state -/
def empty_state : state := λ _ => 0 -- the lambda defines a lambda function

/-! Provide a mechanism to update state -/
def state.update (x : String) (v : Int) (s : state) : state :=
  λ x' => if x' = x then v else s x'

/-! Create custom notation for updating state
    here we are using Lean's macro system to augment its syntax
-/
macro s:term "[" x:term "!->" v:term "]" : term =>
  `(state.update $x $v $s)

#print empty_state -- #print and #eval give you real-time feedback when in an IDE / text editor

def state_ex := empty_state["x" !-> 10]["y" !-> 5]

#eval (state_ex "x")

/-! Define stack and empty stack
    a stack is essentially a linked list so we can use the default 'List' from the standard lib
-/
def stack := List Int
def empty_stack : List Int := []

Syntax

  • Syntax is how a program looks (kindof), it is the way we write our code in a language.
  • for the syntax we will use Backus Naur Form along with Lean’s inductive types.
    • inductive types can be thought of as algebraic data types in languages like Ocaml, Haskell, etc…

BNF

/-! Defining syntax with BNF
        Instr := const Z
          | binop
          | load String
          | set String

        Binop := add
          | minus
          | mult
          | div
-/


/-! Define all binary operations -/
inductive binop : Type where
  | B_Add
  | B_Minus
  | B_Mult
  | B_Div

/-! Define all instructions -/
inductive inst : Type where
  | Const (i: Int)
  | Binop (op : binop)
  | Set   (v : String)
  | Load  (v : String)

/-! Tell Lean how to represent these types so we can see output of #print and #eval -/
instance : Repr binop where
  reprPrec
    | .B_Add, _ => "B_Add"
    | .B_Minus, _ => "B_Minus"
    | .B_Mult, _ => "B_Mult"
    | .B_Div, _ => "B_Div"

instance : Repr inst where
  reprPrec
    | .Const i, _ => "(Const " ++ repr i ++ ")"
    | .Binop op, _ => "(Binop " ++ repr op ++ ")"
    | .Set v, _ => "(Set " ++ repr v ++ ")"
    | .Load v, _ => "(Load " ++ repr v ++ ")"

Semantics

  • the semantics of a language define what something means, if syntax is the structure then semantics is the meaning.
  • for Stack we are using big step semantics, meaning the evaluation function we define doesn’t incrementally evaluate an expression but evaluates the whole thing in one go.
  • to define our semantic rules we show a series of inference rules which will represented by inductive relations which are to inductive types what functions are to types, but in the logical world.

Rules for evaluation

s  := stack
st := state
            
                         s = [ y :: x :: sx ]
         --------------------------------------------------------- (binary operation)
          ([y :: x :: sx], st) =[binop op]=> ((op x y) :: sx, st)


                         s = [ x :: sx ]   v : String
          ---------------------------------------------------- (set operation)
             ([x :: sx], st) =[set v]=> ([sx], st[v !-> x])


                          s : stack    st v = x
          ---------------------------------------------------- (load operation)
                   (s, st) =[load v]=> ((x :: s), st)


                                  x : Int
               --------------------------------------------- (Const)
                    (s, st) =[Const x] => ((x :: s), st)

Functions for evaluation

/-! Evaluation function for binary operations -/
def bo_eval (op : binop) (x y : Int) : Int :=
  match op with
  | .B_Add    => x + y
  | .B_Minus  => x - y
  | .B_Mult   => x * y
  | .B_Div    => x / y

Inductive relations for evaluation

/-! Evaluation relation for a single instruction
    - how our language evaluates one instruction
    - we need cases for each possible type of instruction
    - our inductive relation can be thought of as a function that takes
      an instruction, a tuple of stack and state (evaluation context) and returns
      a new evaluation context and a Prop (this is what makes it an inductive relation)
    - Props are propositions and make this inductive relation a logical proposition, meaning
        we can think of our relation as a logical relation like 'if p then q' but in our case it would be
        - if instruction is x then y
        - we are showing that two evaluation contexts are 'related' by some instruction (hence the name inductive relation)
-/
inductive ieval : inst → (stack × state) → (stack × state) → Prop where
  | I_Const: ∀ (n : Int) (s : stack) (st : state), -- declare an int
    ieval (.Const n) (s, st) ((n :: s), st)
  | I_Binop: ∀ (op : binop) (x y : Int) (s : stack) (st : state), -- perform a binary operation
    ieval (.Binop op) ((y :: x :: s), st) (((bo_eval op x y) :: s), st)
  | I_Set: ∀ (v : String) (x : Int) (s : stack) (st : state), -- set a string to a value in state
    ieval (.Set v) ((x :: s), st) (s, st[v !-> x])
  | I_Load : ∀ (v : String) (x : Int) (s : stack) (st : state), -- load a value from a string
    st v = x → ieval (.Load v) (s, st) ((x :: s), st)

/-! Evaluation relation for a list of instructions
    this completes our evaluation relation as we can now evaluate a list of instructions
-/
inductive seval : List inst → (stack × state) → (stack × state) → Prop where
  | NilI s:
    seval [] s s
  | ConsI i is s s1 s2 st st1 st2:
    ieval i (s, st) (s1, st1) →
    seval is (s1, st1) (s2, st2) →
    seval (i :: is) (s, st) (s2, st2)

Determinism

  • now we get to the reason we used inductive types and relations, so we can prove stuff!
  • we want to show that our language is deterministic, ie same inputs always results in the same outputs.
  • to do this we can show that evaluating one instruction is deterministic and then use that proof to prove evaluating a list of instructions is deterministic.
    • this proof demonstrates how ‘clean’ Lean proofs are and they tend to resemble function definitions.
/-! Show that the execution of one instruction is deterministic -/
theorem ieval_determ {i s s1 s2 st st1 st2}
  (hl : ieval i (s, st) (s1, st1)) -- left hypothesis
  (hr: ieval i (s, st) (s2, st2)): -- right hypothesis
  s1 = s2 ∧ st1 = st2 := -- hypothesis we want to prove, that end states and stacks are equivalent
  by
    -- iterate over all possible instructions instruction
    cases hl
    case I_Const n =>
      cases hr
      -- break apart the ∧ (logical and) and solve both sides
      repeat (any_goals (first | constructor | rfl))
    case I_Binop op x y s' =>
      cases hr
      repeat (any_goals (first | constructor | rfl))
    case I_Set v x =>
      cases hr
      repeat (any_goals (first | constructor | rfl))
    case I_Load v x h =>
      -- match against cases of the right hypothesis
      cases hr
      case I_Load x' h' =>
        -- h  : st v = x
        -- h' : st v = x'
        -- ⊢ ((x :: s) = (x' :: s)) ∧ st = st
        rw [←h, h'] -- rewrite h and h'
        repeat (any_goals (first | constructor | rfl)) -- try to solve any goal with reflection

/-! Show that executing a sequence of instructions is deterministic -/
theorem seval_determ {i s s1 s2 st st1 st2}
  (hl : seval i (s, st) (s1, st1))
  (hr : seval i (s, st) (s2, st2)):
  s1 = s2 ∧ st1 = st2 :=
  by
    -- match against all possible cases for the left hypothesis
    cases hl
    case NilI =>
      cases hr
      case NilI =>
        exact ⟨rfl, rfl⟩ -- apply reflection to both branches of the logical and
    case ConsI i is s1' st1' hi hs =>
      -- match against cases of the right hypothesis
      cases hr
      case ConsI s'' st1'' hi' hs' =>
        -- introduce and prove a new hypothesis, 'h1'
        have h1 : s1' = s'' ∧ st1' = st1'' := by
          apply ieval_determ -- apply the theorem that one instruction is deterministic
          exact hi
          exact hi'
        let ⟨h1l, h1r⟩ := h1 -- break apart logical and in h1
        subst h1r
        subst h1l
        apply seval_determ
        exact hs
        exact hs'