# tsm-lean

A Lean 4 formalization of a Tiny Stack Machine — third concrete kernel parallel to `golang-lean` (TGC) and `octive-lean` (TOC).

The substrate-level asymmetry: TGC and TOC have *named variables*. TSM has values living *by position* on a stack. Forces the cross-language abstraction to factor over "operand-access mechanism" instead of baking name-lookup into the framework. Maps directly to real bytecode targets — WebAssembly, JVM, CPython, .NET CIL, SECD.

## Build

```sh
lake build
```

## Run the demo

```sh
lake exe tsm-lean
# → final stack: [TsmLean.Core.Value.vInt 16]   ((5 + 3) * 2)
# → final pc: 5
```

## Layout

| Path | What's there |
| --- | --- |
| `TsmLean/Core/Syntax.lean`      | `Instr`, `Value`, `Code` |
| `TsmLean/Core/Semantics.lean`   | `State`, `step` (function), `MultiStep` (relation) |
| `TsmLean/Core/Determinism.lean` | `step_deterministic`, `MultiStep.deterministic` |
| `TsmLean/Core/Eval.lean`        | fuel-bounded `run` + `run_sound` |
| `TsmLean/Core/Types.lean`       | `Ty`, `StackTy`, `HasTypeInstr` |
| `TsmLean/Core/TypeSoundness.lean` | `HasTypeV`, `HasTypeStack` |
| `TsmLean/Core/Preservation.lean` | `stack_preservation`, `progress` |
| `Main.lean`                     | demo program |

## Theorems proven

- **`step_deterministic`** — single-step is functional.
- **`MultiStep.deterministic`** — multi-step paths to halted states are unique.
- **`run_sound`** — successful fuel-bounded execution corresponds to a `MultiStep` derivation ending at a halted state.
- **`stack_preservation`** — if the stack matches an instruction's input type and the step succeeds, the post-stack matches its output type.
- **`progress`** — well-typed non-halt instructions always make a step.

The first three are the operational counterparts of the big-step theorems in TGC and TOC. The last two are the small-step type-soundness theorems (Pierce-style), which TGC/TOC's big-step formulations don't have direct analogues for.

Zero sorries, axioms, or admits.

## Status

**v0.1**: per-instruction (local) preservation. Global program-level type soundness — the JVM-style stackmap that ensures all reachable PCs have consistent stack types — is the next layer up.

## Instruction set

```
push n   pushB b   pop   dup   swap
add  sub  mul   eq  lt
jmp k   jmpFalse k   halt
```

Twelve instructions. No call / ret yet — direct jumps only. Adding function-call frames is a future extension.