Compiling IMP to a stack machine

InductiveStack machine instructions#✓fully proved

An instruction of the stack machine is one of \(\mathsf{push}\ n\), \(\mathsf{load}\ x\) and \(\mathsf{store}\ x\) for natural numbers \(n\) and \(x\); the arithmetic instructions \(\mathsf{add}\), \(\mathsf{sub}\) and \(\mathsf{mul}\); the comparison and Boolean instructions \(\mathsf{eq}\), \(\mathsf{le}\), \(\mathsf{not}\) and \(\mathsf{and}\); and the jumps \(\mathsf{jump}\ t\) and \(\mathsf{jumpIfZero}\ t\) for a natural number \(t\). Jump targets are absolute program counters.

inductive Instr where
  | push (n : Nat)
  | load (x : Nat)
  | store (x : Nat)
  | add
  | sub
  | mul
  | eqI
  | leI
  | notI
  | andI
  | jump (target : Nat)
  | jumpIfZero (target : Nat)
  deriving DecidableEq, Repr

Used by 12

Used byCompilation of commands · Compilation of arithmetic expressions · Compiled arithmetic code pushes the value of the expression · Compilation of Boolean expressions · Compiled Boolean code pushes the truth value of the expression · Correctness of compilation to the stack machine · Compiled command code simulates big-step execution · Determinism of the stack machine · Fetching from an embedded code segment · No step past the end of the program · Step relation of the stack machine · Multi-step execution of the stack machine

AbbreviationStack machine configurations#✓fully proved

A configuration of the stack machine is a triple \((pc, \sigma, s)\) of a program counter \(pc \in \mathbb{N}\), a stack \(\sigma\), which is a finite list of natural numbers whose head is the top of the stack, and a state \(s\) assigning a natural number to each variable.

abbrev Config := Nat × List Nat × State

Uses 1 · Used by 8

Statement usesIMP program states

Used byCompiled arithmetic code pushes the value of the expression · Compiled Boolean code pushes the truth value of the expression · Correctness of compilation to the stack machine · Compiled command code simulates big-step execution · Determinism of the stack machine · No step past the end of the program · Step relation of the stack machine · Multi-step execution of the stack machine

InductiveStep relation of the stack machine#✓fully proved

Let \(P\) be a program, that is a list of instructions, and write \(a :: \sigma\) for the stack with top \(a\) above the stack \(\sigma\). A configuration \((pc, \sigma, s)\) steps to a configuration \(c'\) under \(P\) exactly when \(pc < |P|\) and, for the instruction at position \(pc\) of \(P\) (counted from \(0\)), one of the following holds, where \(s[x \mapsto v]\) is the state \(s\) with variable \(x\) set to \(v\).

• \(\mathsf{push}\ n\): \(c' = (pc + 1, n :: \sigma, s)\).
• \(\mathsf{load}\ x\): \(c' = (pc + 1, s(x) :: \sigma, s)\).
• \(\mathsf{store}\ x\): \(\sigma = v :: \tau\) and \(c' = (pc + 1, \tau, s[x \mapsto v])\).
• \(\mathsf{add}\), \(\mathsf{sub}\), \(\mathsf{mul}\): \(\sigma = a :: b :: \tau\) and \(c' = (pc + 1, r :: \tau, s)\), where \(r\) is \(b + a\), \(\max(b - a, 0)\) or \(b \cdot a\) respectively.
• \(\mathsf{eq}\), \(\mathsf{le}\): \(\sigma = a :: b :: \tau\) and \(c' = (pc + 1, r :: \tau, s)\), where \(r\) is \(1\) if \(b = a\), respectively \(b \le a\), and \(r = 0\) otherwise.
• \(\mathsf{not}\): \(\sigma = a :: \tau\) and \(c' = (pc + 1, r :: \tau, s)\), where \(r = 1\) if \(a = 0\) and \(r = 0\) otherwise.
• \(\mathsf{and}\): \(\sigma = a :: b :: \tau\) and \(c' = (pc + 1, r :: \tau, s)\), where \(r = 1\) if \(b \ne 0\) and \(a \ne 0\), and \(r = 0\) otherwise.
• \(\mathsf{jump}\ t\): \(c' = (t, \sigma, s)\).
• \(\mathsf{jumpIfZero}\ t\): either \(\sigma = 0 :: \tau\) and \(c' = (t, \tau, s)\), or \(\sigma = (n + 1) :: \tau\) for some \(n\) and \(c' = (pc + 1, \tau, s)\).

For binary instructions the top of the stack \(a\) is thus the right operand and the value below it \(b\) is the left operand.

Cslib.IMP.StackMachine.Step · 44 lines

inductive Step (prog : List Instr) : Config → Config → Prop
  | push {pc n : Nat} {stack : List Nat} {s : State}
      (hfetch : prog[pc]? = some (.push n)) :
      Step prog (pc, stack, s) (pc + 1, n :: stack, s)
  | load {pc x : Nat} {stack : List Nat} {s : State}
      (hfetch : prog[pc]? = some (.load x)) :
      Step prog (pc, stack, s) (pc + 1, s x :: stack, s)
  | store {pc x v : Nat} {stack : List Nat} {s : State}
      (hfetch : prog[pc]? = some (.store x)) :
      Step prog (pc, v :: stack, s) (pc + 1, stack, Function.update s x v)
  | add {pc a b : Nat} {stack : List Nat} {s : State}
      (hfetch : prog[pc]? = some .add) :
      Step prog (pc, a :: b :: stack, s) (pc + 1, (b + a) :: stack, s)
  | sub {pc a b : Nat} {stack : List Nat} {s : State}
      (hfetch : prog[pc]? = some .sub) :
      Step prog (pc, a :: b :: stack, s) (pc + 1, (b - a) :: stack, s)
  | mul {pc a b : Nat} {stack : List Nat} {s : State}
      (hfetch : prog[pc]? = some .mul) :
      Step prog (pc, a :: b :: stack, s) (pc + 1, (b * a) :: stack, s)
  | eqI {pc a b : Nat} {stack : List Nat} {s : State}
      (hfetch : prog[pc]? = some .eqI) :
      Step prog (pc, a :: b :: stack, s)
        (pc + 1, (if b = a then 1 else 0) :: stack, s)
  | leI {pc a b : Nat} {stack : List Nat} {s : State}
      (hfetch : prog[pc]? = some .leI) :
      Step prog (pc, a :: b :: stack, s)
        (pc + 1, (if b ≤ a then 1 else 0) :: stack, s)
  | notI {pc a : Nat} {stack : List Nat} {s : State}
      (hfetch : prog[pc]? = some .notI) :
      Step prog (pc, a :: stack, s)
        (pc + 1, (if a = 0 then 1 else 0) :: stack, s)
  | andI {pc a b : Nat} {stack : List Nat} {s : State}
      (hfetch : prog[pc]? = some .andI) :
      Step prog (pc, a :: b :: stack, s)
        (pc + 1, (if b ≠ 0 ∧ a ≠ 0 then 1 else 0) :: stack, s)
  | jump {pc target : Nat} {stack : List Nat} {s : State}
      (hfetch : prog[pc]? = some (.jump target)) :
      Step prog (pc, stack, s) (target, stack, s)
  | jumpIfZeroZero {pc target : Nat} {stack : List Nat} {s : State}
      (hfetch : prog[pc]? = some (.jumpIfZero target)) :
      Step prog (pc, 0 :: stack, s) (target, stack, s)
  | jumpIfZeroSucc {pc target n : Nat} {stack : List Nat} {s : State}
      (hfetch : prog[pc]? = some (.jumpIfZero target)) :
      Step prog (pc, (n + 1) :: stack, s) (pc + 1, stack, s)

Uses 3 · Used by 6

Statement usesStack machine configurations · Stack machine instructions · IMP program states

Used byCompiled arithmetic code pushes the value of the expression · Compiled Boolean code pushes the truth value of the expression · Compiled command code simulates big-step execution · Determinism of the stack machine · No step past the end of the program · Multi-step execution of the stack machine

AbbreviationMulti-step execution of the stack machine#✓fully proved

For a program \(P\), the multi-step relation on configurations is the reflexive transitive closure of the step relation of the stack machine running \(P\): it relates \(c\) to \(c'\) when \(c'\) is obtained from \(c\) by zero or more steps.

abbrev Steps (prog : List Instr) : Config → Config → Prop :=
  Relation.ReflTransGen (Step prog)

Uses 3 · Used by 4

Statement usesStack machine configurations · Stack machine instructions · Step relation of the stack machine

Used byCompiled arithmetic code pushes the value of the expression · Compiled Boolean code pushes the truth value of the expression · Correctness of compilation to the stack machine · Compiled command code simulates big-step execution

TheoremDeterminism of the stack machine#✓fully proved

For every program \(P\), the step relation of the stack machine running \(P\) is deterministic: if a configuration \(x\) steps to \(y\) and to \(z\), then \(y = z\). The fetched instruction and the shape of the stack determine the next configuration.

theorem Step.deterministic {prog : List Instr} {x y z : Config}
    (h1 : Step prog x y) (h2 : Step prog x z) : y = z

Uses 4

Statement usesStack machine configurations · Stack machine instructions · Step relation of the stack machine

Proof usesIMP program states

TheoremNo step past the end of the program#✓fully proved

Let \(P\) be a program, that is a list of instructions, and let \((pc, \sigma, s)\) be a configuration with \(|P| \le pc\). Then the stack machine running \(P\) has no step from \((pc, \sigma, s)\) to any configuration, since there is no instruction at position \(pc\) to fetch.

Hence the length of the code compiled from a command at base address \(0\) is a halt address for that code.

theorem no_step_of_length_le {prog : List Instr} {pc : Nat} {stack : List Nat}
    {s : State} (h : prog.length ≤ pc) (y : Config) :
    ¬ Step prog (pc, stack, s) y

Uses 4

Statement usesStack machine configurations · Stack machine instructions · Step relation of the stack machine · IMP program states

DefinitionInstruction count of an arithmetic expression#✓fully proved

The instruction count \(\ell(a)\) of an arithmetic expression \(a\) is defined by recursion on \(a\): a constant or a variable has count \(1\), and if \(a\) is the sum, difference or product of \(a_1\) and \(a_2\), then \(\ell(a) = \ell(a_1) + \ell(a_2) + 1\).

It is the number of stack-machine instructions generated when \(a\) is compiled.

def alen : AExp → Nat
  | .const _ => 1
  | .var _ => 1
  | .add left right => alen left + alen right + 1
  | .sub left right => alen left + alen right + 1
  | .mul left right => alen left + alen right + 1

Uses 1 · Used by 5

Statement usesArithmetic expressions of IMP

Used byInstruction count of a Boolean expression · Instruction count of a command · Compiled arithmetic code pushes the value of the expression · Compiled Boolean code pushes the truth value of the expression · Compiled command code simulates big-step execution

DefinitionInstruction count of a Boolean expression#✓fully proved

The instruction count \(\ell(b)\) of a Boolean expression \(b\) is defined by recursion on \(b\), using the instruction count \(\ell(a)\) of arithmetic expressions \(a\): a truth value has count \(1\); the tests \(a_1 = a_2\) and \(a_1 \le a_2\) have count \(\ell(a_1) + \ell(a_2) + 1\); the negation of \(b_1\) has count \(\ell(b_1) + 1\); and the conjunction of \(b_1\) and \(b_2\) has count \(\ell(b_1) + \ell(b_2) + 1\).

It is the number of stack-machine instructions generated when \(b\) is compiled.

def blen : BExp → Nat
  | .truth _ => 1
  | .eq left right => alen left + alen right + 1
  | .le left right => alen left + alen right + 1
  | .not body => blen body + 1
  | .and left right => blen left + blen right + 1

Uses 3 · Used by 4

Statement usesArithmetic expressions of IMP · Boolean expressions of IMP · Instruction count of an arithmetic expression

Used byInstruction count of a command · Compilation of commands · Compiled Boolean code pushes the truth value of the expression · Compiled command code simulates big-step execution

DefinitionInstruction count of a command#✓fully proved

The instruction count \(\ell(c)\) of an IMP command \(c\) is defined by recursion on \(c\), using the instruction counts \(\ell(a)\) and \(\ell(b)\) of arithmetic and Boolean expressions: \(\ell(\mathbf{skip}) = 0\); \(\ell(x := a) = \ell(a) + 1\); \(\ell(c_1; c_2) = \ell(c_1) + \ell(c_2)\); \(\ell(\mathbf{if}\ b\ \mathbf{then}\ c_1\ \mathbf{else}\ c_2) = \ell(b) + 1 + \ell(c_1) + 1 + \ell(c_2)\); and \(\ell(\mathbf{while}\ b\ \mathbf{do}\ c_1) = \ell(b) + 1 + \ell(c_1) + 1\).

It is the number of stack-machine instructions generated when \(c\) is compiled.

def codeLength : Cmd → Nat
  | .skip => 0
  | .assign _ value => alen value + 1
  | .seq first second => codeLength first + codeLength second
  | .ite guard thenBranch elseBranch =>
      blen guard + 1 + codeLength thenBranch + 1 + codeLength elseBranch
  | .while guard body => blen guard + 1 + codeLength body + 1

Uses 5 · Used by 3

Statement usesArithmetic expressions of IMP · Boolean expressions of IMP · Commands of IMP · Instruction count of an arithmetic expression · Instruction count of a Boolean expression

Used byCompilation of commands · Correctness of compilation to the stack machine · Compiled command code simulates big-step execution

DefinitionCompilation of arithmetic expressions#✓fully proved

The compiled code of an arithmetic expression is the list of stack-machine instructions defined by recursion: a constant \(n\) compiles to the single instruction push \(n\), a variable \(x\) to the single instruction load \(x\), and the sum, difference or product of \(a_1\) and \(a_2\) to the code of \(a_1\), then the code of \(a_2\), then the single instruction add, sub or mul respectively.

Running this code leaves the value of the expression on top of the stack.

def compileA : AExp → List Instr
  | .const value => [.push value]
  | .var name => [.load name]
  | .add left right => compileA left ++ compileA right ++ [.add]
  | .sub left right => compileA left ++ compileA right ++ [.sub]
  | .mul left right => compileA left ++ compileA right ++ [.mul]

Uses 2 · Used by 5

Statement usesArithmetic expressions of IMP · Stack machine instructions

Used byCompilation of commands · Compiled arithmetic code pushes the value of the expression · Compilation of Boolean expressions · Compiled Boolean code pushes the truth value of the expression · Compiled command code simulates big-step execution

DefinitionCompilation of Boolean expressions#✓fully proved

The compiled code of a Boolean expression is the list of stack-machine instructions defined by recursion, using the compiled code of arithmetic expressions: the truth value true compiles to the single instruction push \(1\) and false to push \(0\); the test \(a_1 = a_2\) (respectively \(a_1 \le a_2\)) compiles to the code of \(a_1\), then the code of \(a_2\), then the equality (respectively order) test instruction; the negation of \(b_1\) compiles to the code of \(b_1\) followed by the negation instruction; and the conjunction of \(b_1\) and \(b_2\) compiles to the code of \(b_1\), then the code of \(b_2\), then the conjunction instruction.

Running this code leaves \(1\) (true) or \(0\) (false) on top of the stack.

def compileB : BExp → List Instr
  | .truth value => [.push (cond value 1 0)]
  | .eq left right => compileA left ++ compileA right ++ [.eqI]
  | .le left right => compileA left ++ compileA right ++ [.leI]
  | .not body => compileB body ++ [.notI]
  | .and left right => compileB left ++ compileB right ++ [.andI]

Uses 4 · Used by 3

Statement usesArithmetic expressions of IMP · Boolean expressions of IMP · Stack machine instructions · Compilation of arithmetic expressions

Used byCompilation of commands · Compiled Boolean code pushes the truth value of the expression · Compiled command code simulates big-step execution

DefinitionCompilation of commands#✓fully proved

The compiled code \(C_p(c)\) of an IMP command \(c\) at base program counter \(p\) is the list of stack-machine instructions defined by recursion on \(c\), where jump targets are absolute program counters and \(\ell\) denotes instruction counts: \(C_p(\mathbf{skip})\) is empty; \(C_p(x := a)\) is the code of \(a\) followed by the instruction store \(x\); \(C_p(c_1; c_2)\) is \(C_p(c_1)\) followed by \(C_{p + \ell(c_1)}(c_2)\). For the conditional \(\mathbf{if}\ b\ \mathbf{then}\ c_1\ \mathbf{else}\ c_2\), put \(q = p + \ell(b) + 1\) and \(r = q + \ell(c_1) + 1\); its code is the code of \(b\), then jump-if-zero to \(r\), then \(C_q(c_1)\), then jump to \(r + \ell(c_2)\), then \(C_r(c_2)\). For the loop \(\mathbf{while}\ b\ \mathbf{do}\ c_1\), put \(q = p + \ell(b) + 1\); its code is the code of \(b\), then jump-if-zero to \(q + \ell(c_1) + 1\), then \(C_q(c_1)\), then jump to \(p\).

Cslib.IMP.StackMachine.compile · 16 lines

def compile : Cmd → Nat → List Instr
  | .skip, _ => []
  | .assign name value, _ => compileA value ++ [.store name]
  | .seq first second, pc =>
      compile first pc ++ compile second (pc + codeLength first)
  | .ite guard thenBranch elseBranch, pc =>
      compileB guard ++
        [.jumpIfZero (pc + blen guard + 1 + codeLength thenBranch + 1)] ++
        compile thenBranch (pc + blen guard + 1) ++
        [.jump (pc + blen guard + 1 + codeLength thenBranch + 1 +
          codeLength elseBranch)] ++
        compile elseBranch (pc + blen guard + 1 + codeLength thenBranch + 1)
  | .while guard body, pc =>
      compileB guard ++
        [.jumpIfZero (pc + blen guard + 1 + codeLength body + 1)] ++
        compile body (pc + blen guard + 1) ++ [.jump pc]

Uses 8 · Used by 2

Statement usesArithmetic expressions of IMP · Boolean expressions of IMP · Commands of IMP · Stack machine instructions · Instruction count of a Boolean expression · Instruction count of a command · Compilation of arithmetic expressions · Compilation of Boolean expressions

Used byCorrectness of compilation to the stack machine · Compiled command code simulates big-step execution

TheoremFetching from an embedded code segment#✓fully proved

Let \(B\), \(S\) and \(A\) be lists of instructions and let \(i < |S|\) be a natural number. Then the instruction at position \(|B| + i\) of the concatenation \(B\,S\,A\) of the three lists equals the instruction at position \(i\) of \(S\), positions being counted from \(0\).

theorem fetch_segment {before seg after : List Instr} {i : Nat}
    (hi : i < seg.length) :
    (before ++ seg ++ after)[before.length + i]? = seg[i]?

Uses 1 · Used by 3

Statement usesStack machine instructions

Used byCompiled arithmetic code pushes the value of the expression · Compiled Boolean code pushes the truth value of the expression · Compiled command code simulates big-step execution

TheoremCompiled arithmetic code pushes the value of the expression#✓fully proved

Let \(a\) be an arithmetic expression with compiled code \(C(a)\) and instruction count \(\ell(a)\), let \(P\) and \(Q\) be lists of instructions, \(\sigma\) a stack and \(s\) a state, and write \(|P|\) for the length of \(P\). The stack machine running the program \(P \, C(a) \, Q\) (the concatenation of \(P\), \(C(a)\) and \(Q\)) goes in finitely many steps from program counter \(|P|\), stack \(\sigma\) and state \(s\) to program counter \(|P| + \ell(a)\), the stack obtained from \(\sigma\) by pushing the value of \(a\) in \(s\), and the same state \(s\).

theorem compileA_runs {a : AExp} {before after : List Instr} {stack : List Nat}
    {s : State} :
    Steps (before ++ compileA a ++ after) (before.length, stack, s)
      (before.length + alen a, a.eval s :: stack, s)

Uses 10 · Used by 2

Statement usesArithmetic expressions of IMP · Evaluation of IMP arithmetic expressions · Stack machine instructions · Multi-step execution of the stack machine · Instruction count of an arithmetic expression · Compilation of arithmetic expressions · IMP program states

Proof usesStack machine configurations · Step relation of the stack machine · Fetching from an embedded code segment

Used byCompiled Boolean code pushes the truth value of the expression · Compiled command code simulates big-step execution

TheoremCompiled Boolean code pushes the truth value of the expression#✓fully proved

Let \(b\) be a Boolean expression with compiled code \(C(b)\) and instruction count \(\ell(b)\), let \(P\) and \(Q\) be lists of instructions, \(\sigma\) a stack and \(s\) a state, and write \(|P|\) for the length of \(P\). The stack machine running the program \(P \, C(b) \, Q\) (the concatenation of \(P\), \(C(b)\) and \(Q\)) goes in finitely many steps from program counter \(|P|\), stack \(\sigma\) and state \(s\) to program counter \(|P| + \ell(b)\), the stack obtained from \(\sigma\) by pushing \(1\) if \(b\) evaluates to true in \(s\) and \(0\) otherwise, and the same state \(s\).

theorem compileB_runs {b : BExp} {before after : List Instr} {stack : List Nat}
    {s : State} :
    Steps (before ++ compileB b ++ after) (before.length, stack, s)
      (before.length + blen b, cond (b.eval s) 1 0 :: stack, s)

Uses 15 · Used by 1

Statement usesBoolean expressions of IMP · Evaluation of IMP Boolean expressions · Stack machine instructions · Multi-step execution of the stack machine · Instruction count of a Boolean expression · Compilation of Boolean expressions · IMP program states

Proof usesArithmetic expressions of IMP · Evaluation of IMP arithmetic expressions · Stack machine configurations · Step relation of the stack machine · Instruction count of an arithmetic expression · Compilation of arithmetic expressions · Compiled arithmetic code pushes the value of the expression · Fetching from an embedded code segment

Used byCompiled command code simulates big-step execution

TheoremCompiled command code simulates big-step execution#✓fully proved

Let \(c\) be a command and \(s\), \(s'\) states such that \(c\) run from \(s\) terminates in \(s'\) under the big-step semantics. Let \(P\) and \(Q\) be lists of instructions, \(\sigma\) a stack, \(|P|\) the length of \(P\), \(C_p(c)\) the compiled code of \(c\) at base program counter \(p\), and \(\ell(c)\) the instruction count of \(c\). Then the stack machine running the program \(P \, C_{|P|}(c) \, Q\) (the concatenation of \(P\), \(C_{|P|}(c)\) and \(Q\)) goes in finitely many steps from program counter \(|P|\), stack \(\sigma\) and state \(s\) to program counter \(|P| + \ell(c)\), the same stack \(\sigma\) and state \(s'\).

theorem compile_runs {c : Cmd} {s s' : State} (h : BigStep c s s')
    {before after : List Instr} {stack : List Nat} :
    Steps (before ++ compile c before.length ++ after) (before.length, stack, s)
      (before.length + codeLength c, stack, s')

Uses 20 · Used by 1

Statement usesBig-step semantics of IMP · Commands of IMP · Stack machine instructions · Multi-step execution of the stack machine · Instruction count of a command · Compilation of commands · IMP program states

Proof usesArithmetic expressions of IMP · Evaluation of IMP arithmetic expressions · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · Stack machine configurations · Step relation of the stack machine · Instruction count of an arithmetic expression · Instruction count of a Boolean expression · Compilation of arithmetic expressions · Compiled arithmetic code pushes the value of the expression · Compilation of Boolean expressions · Compiled Boolean code pushes the truth value of the expression · Fetching from an embedded code segment

Used byCorrectness of compilation to the stack machine

TheoremCorrectness of compilation to the stack machine#✓fully proved

Let \(c\) be a command and \(s\), \(s'\) states such that \(c\) run from \(s\) terminates in \(s'\) under the big-step semantics. Let \(C_0(c)\) be the compiled code of \(c\) at base program counter \(0\) and \(\ell(c)\) the instruction count of \(c\). Then the stack machine running \(C_0(c)\) goes in finitely many steps from program counter \(0\), the empty stack and state \(s\) to program counter \(\ell(c)\), the empty stack and state \(s'\).

Since \(C_0(c)\) has exactly \(\ell(c)\) instructions, no step is possible at program counter \(\ell(c)\), so the machine halts there. Only this forward simulation is claimed, not its converse.

theorem compile_correct {c : Cmd} {s s' : State} (h : BigStep c s s') :
    Steps (compile c 0) (0, [], s) (codeLength c, [], s')

Uses 9

Statement usesBig-step semantics of IMP · Commands of IMP · Multi-step execution of the stack machine · Instruction count of a command · Compilation of commands · IMP program states

Proof usesStack machine configurations · Stack machine instructions · Compiled command code simulates big-step execution

17 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.